diff options
author | Francesco Mazzoli <f@mazzo.li> | 2013-06-10 17:03:52 +0100 |
---|---|---|
committer | Francesco Mazzoli <f@mazzo.li> | 2013-06-10 17:03:52 +0100 |
commit | 220ca85e4c690269298b9e8c1ef1752fad285855 (patch) | |
tree | 8a5baaec4bd038e8af7966c49e21b4ea8c0a22a4 /itt.ka | |
parent | 2a33412a41393afc6574354625c0d9434f099754 (diff) |
...
Diffstat (limited to 'itt.ka')
-rw-r--r-- | itt.ka | 17 |
1 files changed, 17 insertions, 0 deletions
@@ -0,0 +1,17 @@ +data Empty : * => { } + +absurd [A : *] [x : Empty] : A => ( + Empty-Elim x (\_ => A) +) + +neg [A : *] : * => (A -> Empty) + +record Unit : * => tt { } + +record Prod : [A : *] [B : A -> *] -> * => + prod {fst : A, snd : B fst} + +data Bool : * => { true : Bool | false : Bool } + +-- The if_then_else_ is provided by Bool-Elim + |