blob: e9decf6bb4a19d72bdfd3de644adc9827246afa4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
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
|
