Commit 7891aa0b authored by Robbert Krebbers's avatar Robbert Krebbers

Also type classes for conjunction and unit.

parent 1bbe31fe
......@@ -35,6 +35,14 @@ Existing Class Or.
Existing Instance Or_l | 9.
Existing Instance Or_r | 10.
Inductive And (P1 P2 : Type) := And_intro : P1 P2 And P1 P2.
Existing Class And.
Existing Instance And_intro.
Inductive Unit := Unit_intro : Unit.
Existing Class Unit.
Existing Instance Unit_intro.
(** Throughout this development we use [C_scope] for all general purpose
notations that do not belong to a more specific scope. *)
Delimit Scope C_scope with C.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment