Skip to content
Snippets Groups Projects
Commit f88fe7a6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Apply suggestion to tests/notation.v

parent f5ed12e1
No related branches found
No related tags found
No related merge requests found
From stdpp Require Import base tactics. From stdpp Require Import base tactics.
(** Test parsing of variants of [(≡)] notation. *) (** Test parsing of variants of [(≡)] notation. *)
Lemma test_equiv_annot_sections `{!Equiv A, Equivalence A (≡@{A})} (x : A) : Lemma test_equiv_annot_sections `{!Equiv A, !Equivalence (≡@{A})} (x : A) :
x ≡@{A} x (≡@{A}) x x (x .) x (. x) x x ≡@{A} x (≡@{A}) x x (x .) x (. x) x
((x ≡@{A} x)) ((≡@{A})) x x ((x .)) x ((. x)) x ((x ≡@{A} x)) ((≡@{A})) x x ((x .)) x ((. x)) x
( x ≡@{A} x) ( x .) x ( x ≡@{A} x) ( x .) x
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment