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...