Question says it all, this is the intervals I am trying to see how can they be done:
From my basic knowledge,
0 = 1: I feels like it breaks the inversion principle in Coq, so if one tried to formalize that and assuming that induction types are not going to work, what will be the way to go ?
Edit: I found this:
Private Inductive interval : Type0 := | zero : interval | one : interval. Axiom seg : zero = one.
This looks scary, doesn't
seg -> False already?
Last updated: Dec 07 2023 at 17:01 UTC