Stream: Equations devs & users

Topic: Compatibility with ssreflect

view this post on Zulip Ayumu Saito (Apr 15 2022 at 02:07):

How can I avoid this error?

Require Import ssreflect ssrbool ssrfun.
Require PeanoNat.

Lemma tmp (n : nat) : n + O = n.
Proof.
by rewrite ?(PeanoNat.Nat.add_0_r, PeanoNat.Nat.add_0_r).
Qed.

From Equations Require Import Equations.

Lemma tmp_ (n : nat) : n + O = n.
Proof.
rewrite ?(PeanoNat.Nat.add_0_r, PeanoNat.Nat.add_0_r).
(* Syntax error: ')' expected after [term level 200] (in [term]). *)

view this post on Zulip Paolo Giarrusso (Apr 15 2022 at 09:02):

maybe add a space, like rewrite ? ( ? That helps if Equations made ?( a single token

Last updated: May 28 2023 at 18:29 UTC