blob: 3a2548dddc7c2fbcf2210811b55bf6574d5f082d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
true ? 0; 1
: nat
if true as x return (x ? nat; bool) then 0 else true
: true ? nat; bool
Defining 'proj1' as keyword
fun e : nat * nat => proj1 e
: nat * nat -> nat
Defining 'decomp' as keyword
decomp (true, true) as t, u in (t, u)
: bool * bool
!(0 = 0)
: Prop
forall n : nat, n = 0
: Prop
!(0 = 0)
: Prop
|
