git.iko.soy/Idris-dev
on 75e0141 help sign in
Idris-dev/lib/Language/Reflection.idr
19 lines 491 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 | GoalType TTName Tactic -- only run if the goal has the right type
14 | Refine TTName
15 | Seq Tactic Tactic
16 | Trivial
17 | Solve
18 | Exact TT -- not yet implemented