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

Merge branch 'test-equiv' into 'master'

Add tests for equiv notation

See merge request !143
parents b5f67e55 f88fe7a6
No related branches found
No related tags found
No related merge requests found
From stdpp Require Import base tactics.
(** Test parsing of variants of [(≡)] notation. *)
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) ( x .) x
(x ≡@{A} x ) (≡@{A} ) x x (. x ) x.
Proof. naive_solver. Qed.
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