diff options
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 + |