-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathdesired.txt
82 lines (56 loc) · 3.15 KB
/
desired.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
transport : ∀ {A : Set} {P : A → Set} {x y : A} (p : x ≡ y) → P x → P y
transport {A} {P} {x} {y} = J D d x y
where
D : (x y : A) → x ≡ y → Set
D x y p = P x → P y
d : (x : A) → D x x r
d = λ x → id
funExt (A : U) (B : A -> U) (f g : (x : A) -> B x) (p : (x : A) -> Path (B x) (f x) (g x)) : Path ((y : A) -> B y) f g = undefined
<i> \(a : A) -> (p a) @ i
Exp> DeclUndef FunExt (ConsTele (TeleC A BaseAIdent Univ) (ConsTele (TeleC B BaseAIdent (Fun (Var A) Univ)) (ConsTele (TeleC F (ConsAIdent G BaseAIdent) (Pi (BasePTele (PTeleC (Var X) (Var A))) (App (Var B) (Var X)))) (ConsTele (TeleC P BaseAIdent (Pi (BasePTele (PTeleC (Var X) (Var A))) (Id (App (Var B) (Var X)) (App (Var F) (Var X)) (App (Var G) (Var X))))) BaseTele)))) (Id (Pi (BasePTele (PTeleC (Var Y) (Var A))) (App (Var B) (Var Y))) (Var F) (Var G))
equalNat : nat → nat → bool
equalNat zero zero = true
equalNat zero (suc n2) = false
equalNat (suc n1) zero = false
equalNat (suc n1) (suc n2) = equalNat n1 n2
equalNat : nat -> nat -> bool = split
zero -> split@ ( nat -> bool ) with
zero -> true
suc n -> false
suc m -> split@ ( nat -> bool ) with
zero -> false
suc n -> equalNat m n
DeclSplit
(AIdent ((113,1),"equalNat"))
[]
(Fun (Var (AIdent ((113,12),"nat"))) (Fun (Var (AIdent ((113,19),"nat"))) (Var (AIdent ((113,26),"bool")))))
[OBranch
(AIdent ((114,5),"zero"))
[]
(NoWhere
(Split (Fun (Var (AIdent ((114,20),"nat"))) (Var (AIdent ((114,27),"bool")))) [OBranch (AIdent ((115,7),"zero")) [] (NoWhere (Var (AIdent ((115,16),"true")))),OBranch (AIdent ((116,7),"suc")) [AIdent ((116,11),"n")] (NoWhere (Var (AIdent ((116,16),"false"))))]))
,
OBranch (AIdent ((117,5),"suc")) [AIdent ((117,9),"m")] (NoWhere (Split (Fun (Var (AIdent ((117,21),"nat"))) (Var (AIdent ((117,28),"bool")))) [OBranch (AIdent ((118,7),"zero")) [] (NoWhere (Var (AIdent ((118,16),"false")))),OBranch (AIdent ((119,7),"suc")) [AIdent ((119,11),"n")] (NoWhere (App (App (Var (AIdent ((119,16),"equalNat"))) (Var (AIdent ((119,25),"m")))) (Var (AIdent ((119,27),"n")))))]))]
p "equalNat : top -> nat -> bool = split unit -> split@ ( nat -> bool ) with zero -> true || suc n -> false"
DeclSplit EqualNat BaseTele (Fun (Var Top) (Fun (Var Nat) (Var Bool))) (BaseBranch (OBranch Unit BaseAIdent (NoWhere
(Split
(Fun (Var Nat) (Var Bool))
(ConsBranch
(OBranch Zero BaseAIdent (NoWhere (Var True)))
(BaseBranch
(OBranch Suc (ConsAIdent N BaseAIdent) (NoWhere (Var False))))))
)))
p "equalNat : top -> nat -> bool = split unit -> split@ ( nat -> bool ) with zero -> true || suc n -> false"
DeclSplit EqualNat BaseTele (Fun (Var Top) (Fun (Var Nat) (Var Bool)))
(ConsBranch
(OBranch Unit BaseAIdent (NoWhere (Split (Fun (Var Nat) (Var Bool)) (BaseBranch (OBranch Zero BaseAIdent (NoWhere (Var True)))))))
(BaseBranch (OBranch Suc (ConsAIdent N BaseAIdent) (NoWhere (Var False)))))
data Vec (A : Set) : Nat -> Set where
[] : Vec A 0
Cons : A -> Vec A n -> Vec a (n+1)
data Bool : Set where
true : Bool
false : Bool
caseBool ( x : U ) ( y z : x ) : bool -> U
caseBool false = y
caseBool true = z