blob: 740e08a7b8efebbf85cbfa527709e8054564ab62 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
data Cat : Type where
VarOrWild : Cat
Exp : Cat
Ident : Cat
data Tree : Cat -> Type where
EAbs : Tree VarOrWild -> Tree Exp -> Tree Exp
EPi : Tree VarOrWild -> Tree Exp -> Tree Exp -> Tree Exp
EVar : Tree Ident -> Tree Exp
EType : Tree Exp
EStr : String -> Tree Exp
EInt : Integer -> Tree Exp
VVar : Tree Ident -> Tree VarOrWild
VWild : Tree VarOrWild
Ident : String -> Tree Ident
f e = case e of
EAbs (VWild || VVar _) e || EPi (VWild || VVar _) _ e -> doSomething e
Ident i -> Ident i
_ -> catchAll
g (Ident x || EAbs (VWild || VVar _) t e) = x e
|
