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

Merge branch 'ralf/empty' into 'master'

add Equiv instance for Empty_set

See merge request !89
parents adfc24d2 12f82ad7
No related branches found
No related tags found
1 merge request!89add Equiv instance for Empty_set
Pipeline #19348 passed
......@@ -591,6 +591,13 @@ Instance unit_leibniz : LeibnizEquiv unit.
Proof. intros [] []; reflexivity. Qed.
Instance unit_inhabited: Inhabited unit := populate ().
(** ** Empty *)
Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True.
Instance Empty_set_equivalence : Equivalence (≡@{Empty_set}).
Proof. repeat split. Qed.
Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
Proof. intros [] []; reflexivity. Qed.
(** ** Products *)
Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope.
Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
......
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