@@ -60,33 +60,46 @@ intEq x y = case x == y of
6060
6161-- | A tactic script to run intEq on two let-bound or introduced
6262-- arguments of the current (otherwise empty) proof context
63−firstEq : List (TTName, Binder TT) -> Tactic
64−firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) = Exact (App (App f x) y)
65−firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
66−firstEq xs = Exact (TConst (I 0))
63+firstEq : List (TTName, Binder TT) -> TT -> Tactic
64+firstEq ((_, (Let _ y))::(_, (Let _ x))::(_, Let _ f)::Nil) _ = Exact (App (App f x) y)
65+firstEq ((y, Lam yt)::(x, Lam xt)::(_, Let _ f)::Nil) _ = Exact (App (App f (P (Bound) x xt)) (P Bound y yt))
66+firstEq xs _ = Exact (TConst (I 0))
6767
6868-- | Skip 3 arguments of the proof context and return the fourth one which
6969-- has to be introduced.
7070-- Used for the tactical dispatch example, which will push dispatch,
71−-- its current proof context and the result of dispatch applied to it
71+-- its current proof context, the goal, and the result of dispatch applied to it
7272-- first.
73−innerTac : List (TTName, Binder TT) -> Tactic
74−innerTac (_::_::_::(x, Lam xt)::_) = Exact (P Bound x xt)
73+innerTac : List (TTName, Binder TT) -> TT -> Tactic
74+innerTac (_::_::_::_::(x, Lam xt)::_) _ = Exact (P Bound x xt)
7575
7676-- | Returns the reflected representation of innerTac
7777innerTacTT : TT
7878innerTacTT = ?innerTacTTPrf
7979
8080-- | Dispatch to the reflected rep. of innerTac
81−dispatch : List (TTName, Binder TT) -> Tactic
82−dispatch xs = ApplyTactic (innerTacTT)
81+dispatch : List (TTName, Binder TT) -> TT -> Tactic
82+dispatch xs _ = ApplyTactic (innerTacTT)
8383
8484-- | Call dispatch which will then dispatch to innerTac.
8585tacticalDispatch : Int -> Int
8686tacticalDispatch = ?tacticalDispatchPrf
8787
88+-- | A tactic to get the representation of its goal
89+studyGoalTac : List (TTName, Binder TT) -> TT -> Tactic
90+studyGoalTac _ goal = Reflect goal
91+
92+-- | Returns the representation of its goal, TT
93+-- (so this is reflect on the type TT)
94+studyGoal : TT
95+studyGoal = ?studyGoalPrf
96+
8897---------- Proofs ----------
8998
99+ReflectionExamples.studyGoalPrf = proof {
100+ applyTactic studyGoalTac;
101+}
102+
90103ReflectionExamples.envTuplePrf = proof {
91104 let x = tupleType;
92105 fill x;