Commit 6c34b059 authored by Robbert Krebbers's avatar Robbert Krebbers

Put `TCIf` in `Prop`.

parent 28e72e3c
...@@ -67,7 +67,7 @@ as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to ...@@ -67,7 +67,7 @@ as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
establish [R], i.e. does not have the behavior of a conditional. Furthermore, establish [R], i.e. does not have the behavior of a conditional. Furthermore,
note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally
would not be able to prove the negation of [P]. *) would not be able to prove the negation of [P]. *)
Inductive TCIf (P Q R : Prop) := Inductive TCIf (P Q R : Prop) : Prop :=
| TCIf_true : P Q TCIf P Q R | TCIf_true : P Q TCIf P Q R
| TCIf_false : R TCIf P Q R. | TCIf_false : R TCIf P Q R.
Existing Class TCIf. Existing Class TCIf.
......
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