Simon Génier pushed to branch simon-genier at Stefan / Typer
Commits: 03f6a3b2 by Simon Génier at 2019-09-25T21:23:14Z Add eliminators for Pair in pervasive.typer.
- - - - - a8096766 by Simon Génier at 2019-09-25T21:23:42Z Add datacons' for Decidable.
- - - - -
1 changed file:
- btl/pervasive.typer
Changes:
===================================== btl/pervasive.typer ===================================== @@ -386,6 +386,12 @@ BoolMod = (##datacons Pair = typecons (Pair (a : Type) (b : Type)) (pair (fst : a) (snd : b)); pair = datacons Pair pair;
+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; + __.__ = let mksel o f = let constructor = Sexp_node (Sexp_symbol "##datacons") @@ -452,11 +458,10 @@ Not : Type -> Type; Not prop = prop -> False;
%% 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) +;
%% Testing generalization in inductive type constructors. LList : (a : Type) -> Int -> Type; %FIXME: `LList : ?` should be sufficient!
View it on GitLab: https://gitlab.com/monnier/typer/compare/f64ab3da85ca3d8b8d8d7aa7cb2b75d37f4...
Afficher les réponses par date
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