Commit 5c857c01 authored by Robbert Krebbers's avatar Robbert Krebbers

Prefix logical operators on the type class level with TC.

parent fa6ff9d1
...@@ -28,20 +28,20 @@ Unset Primitive Projections. ...@@ -28,20 +28,20 @@ Unset Primitive Projections.
(* The [Or] class is useful for efficiency: instead of having two instances (* The [Or] class is useful for efficiency: instead of having two instances
[P → Q1 → R] and [P → Q2 → R] we could have one instance [P → Or Q1 Q2 → R], [P → Q1 → R] and [P → Q2 → R] we could have one instance [P → Or Q1 Q2 → R],
which avoids the need to derive [P] twice. *) which avoids the need to derive [P] twice. *)
Inductive Or (P1 P2 : Type) := Inductive TCOr (P1 P2 : Type) :=
| Or_l : P1 Or P1 P2 | TCOr_l : P1 TCOr P1 P2
| Or_r : P2 Or P1 P2. | TCOr_r : P2 TCOr P1 P2.
Existing Class Or. Existing Class TCOr.
Existing Instance Or_l | 9. Existing Instance TCOr_l | 9.
Existing Instance Or_r | 10. Existing Instance TCOr_r | 10.
Inductive And (P1 P2 : Type) := And_intro : P1 P2 And P1 P2. Inductive TCAnd (P1 P2 : Type) := TCAnd_intro : P1 P2 TCAnd P1 P2.
Existing Class And. Existing Class TCAnd.
Existing Instance And_intro. Existing Instance TCAnd_intro.
Inductive Unit := Unit_intro : Unit. Inductive TCUnit := TCUnit_intro : TCUnit.
Existing Class Unit. Existing Class TCUnit.
Existing Instance Unit_intro. Existing Instance TCUnit_intro.
(** Throughout this development we use [C_scope] for all general purpose (** Throughout this development we use [C_scope] for all general purpose
notations that do not belong to a more specific scope. *) notations that do not belong to a more specific scope. *)
......
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