[Git][monnier/typer][simon-genier] 2 commits: Add eliminators for Pair in pervasive.typer.
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... -- View it on GitLab: https://gitlab.com/monnier/typer/compare/f64ab3da85ca3d8b8d8d7aa7cb2b75d37f4... You're receiving this email because of your account on gitlab.com.
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
participants (2)
-
Simon Génier -
Stefan Monnier