2014-12-12 13:17:50 -05:00
|
|
|
--javra: Maybe this should go somewhere else
|
2014-12-11 23:14:53 -05:00
|
|
|
|
2014-12-12 13:17:50 -05:00
|
|
|
open eq
|
2014-12-16 14:22:54 -05:00
|
|
|
|
2014-12-11 23:14:53 -05:00
|
|
|
inductive tdecidable [class] (A : Type) : Type :=
|
|
|
|
|
inl : A → tdecidable A,
|
2014-12-16 14:22:54 -05:00
|
|
|
inr : ¬A → tdecidable A
|
2014-12-11 23:14:53 -05:00
|
|
|
|
|
|
|
|
structure decidable_paths [class] (A : Type) :=
|
2014-12-12 13:17:50 -05:00
|
|
|
(elim : ∀(x y : A), tdecidable (x = y))
|
