git.iko.soy/Idris-dev
on 1ffdfc0 help sign in
Idris-dev/lib/Language/Reflection.idr
18 lines 411 B history raw
1module Language.Reflection
3TTName : Type
4TTName = String -- needs to capture namespaces too...
6data TT = Var TTName
7 | Lam TTName TT TT
8 | Pi TTName TT TT
9 | Let TTName TT TT TT
10 | App TTName TT TT
12data Tactic = Try Tactic Tactic
13 | Refine TTName
14 | Seq Tactic Tactic
15 | Trivial
16 | Solve
17 | Exact TT -- not yet implemented