Salut Simon,
Quelques commentaires sur ton patch:
+fst : (a : Type) ≡> (b : Type) ≡> Pair a b -> a; +fst p = case p | pair l _ => l;
+snd : (a : Type) ≡> (b : Type) ≡> Pair a b -> b; +snd p = case p | pair _ r => r;
The Pair type is on the way out (replaced by tuples, see tuple.typer).
%% Like Bool, except that it additionally carries the meaning of its value. -%% We don't use the `type` macro here because it would make these `true` -%% and `false` constructors ovrride `Bool`'s, and we currently don't -%% want that. -Decidable = typecons (Decidable (prop : Type))
(true (p ::: prop)) (false (p ::: Not prop));
+type Decidable (prop : Type)
- | yes (p ::: prop)
- | no (p ::: Not prop)
+;
Note the "currently" in the comment you removed. The intention once we have type classes working is to make `if` work on `Decidable` rather than on `Bool` (and basically never use `Bool`).
More specifically, `if` should take a "Prop" argument (rather than a `Decidable` or `Bool` argument), then find the corresponding decision procedure (via type classes) and use that to compute the condition. Then each branch will get the proof of the Prop or its negation.
Part of the reason for this approach is avoid tensions in the choice of names (should `a < b` be the thing of type `Prop` or the thing of type `bool`?)
Stefan