@@ -9,7 +9,7 @@ using (xs : List a, ys : List a, G : List (List a))
99 Stop : Elem x (x :: xs)
1010 Pop : Elem x ys -> Elem x (y :: xs)
1111
12−-- Expr is a Reflection of a list, indexed over the concrete list,
12+-- Expr is a reflection of a list, indexed over the concrete list,
1313-- and over a set of list variables.
1414
1515 data Expr : List (List a) -> List a -> Type where
@@ -76,7 +76,7 @@ using (xs : List a, ys : List a, G : List (List a))
7676 eqExpr ENil ENil = Just Refl
7777 eqExpr _ _ = Nothing
7878
79−-- Given a couple of Reflected expressions, try to produce a proof that
79+-- Given a couple of reflected expressions, try to produce a proof that
8080-- they are equal
8181
8282 buildProof : {xs : List a} -> {ys : List a} ->
@@ -91,7 +91,7 @@ using (xs : List a, ys : List a, G : List (List a))
9191 let (rn ** (r', rPrf)) = reduce r in
9292 buildProof l' r' lPrf rPrf
9393
94−-- Given a Reflected equality, try to produce a proof that holds
94+-- Given a reflected equality, try to produce a proof that holds
9595
9696 prove : ListEq G t -> Maybe t
9797 prove (EqP xs ys) = testEq xs ys
@@ -103,7 +103,7 @@ using (xs : List a, ys : List a, G : List (List a))
103103-- Some helpers for later... 'prim__syntactic_eq' is a primitive which
104104-- (at compile-time only) attempts to construct a proof that its arguments
105105-- are syntactically equal. We'll find this useful for referring to variables
106−-- in Reflected terms.
106+-- in reflected terms.
107107
108108 isElem : (x : a) -> (xs : List a) -> Maybe (Elem x xs)
109109 isElem x [] = Nothing
@@ -122,44 +122,44 @@ using (xs : List a, ys : List a, G : List (List a))
122122 weaken G' ENil = ENil
123123
124124
125−-- Now, some Reflection magic.
126−-- %Reflection means a function runs on syntax, rather than on constructors.
127−-- So, 'ReflectList' builds a Reflected List expression as defined above.
125+-- Now, some reflection magic.
126+-- %reflection means a function runs on syntax, rather than on constructors.
127+-- So, 'reflectList' builds a reflected List expression as defined above.
128128
129−-- It also converts (x :: xs) into a Reflected [x] ++ xs so that the above
129+-- It also converts (x :: xs) into a reflected [x] ++ xs So that the above
130130-- reduction will work the right way.
131131
132−%Reflection
133−ReflectList : (G : List (List a)) ->
132+%reflection
133+reflectList : (G : List (List a)) ->
134134 (xs : List a) -> (G' ** Expr (G' ++ G) xs)
135−ReflectList G [] = ([] ** ENil)
135+reflectList G [] = ([] ** ENil)
136136
137−ReflectList G (x :: xs) with (ReflectList G xs)
137+reflectList G (x :: xs) with (reflectList G xs)
138138 | (G' ** xs') with (isElem (List.(::) x []) (G' ++ G))
139139 | Just p = (G' ** App (Var p) xs')
140140 | Nothing = ([x] :: G' ** App (Var Stop) (weaken [[x]] xs'))
141141
142−ReflectList G (xs ++ ys) with (ReflectList G xs)
143− | (G' ** xs') with (ReflectList (G' ++ G) ys)
142+reflectList G (xs ++ ys) with (reflectList G xs)
143+ | (G' ** xs') with (reflectList (G' ++ G) ys)
144144 | (G'' ** ys') = ((G'' ++ G') **
145145 rewrite (sym (appendAssociative G'' G' G)) in
146146 App (weaken G'' xs') ys')
147−ReflectList G t with (isElem t G)
147+reflectList G t with (isElem t G)
148148 | Just p = ([] ** Var p)
149149 | Nothing = ([t] ** Var Stop)
150150
151151
152−-- Similarly, ReflectEq converts an equality proof on Lists into the ListEq
153−-- Reflection. Note that it isn't total, and we have to give the element type
152+-- Similarly, reflectEq converts an equality proof on Lists into the ListEq
153+-- reflection. Note that it isn't total, and we have to give the element type
154154-- explicitly because it can't be inferred from P.
155155
156−-- This is not really a problem - we'll want different Reflections for different
156+-- This is not really a problem - we'll want different reflections for different
157157-- forms of equality proofs anyway.
158158
159−%Reflection
160−ReflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)
161−ReflectEq a G (the (List a) xs = the (List a) ys) with (ReflectList G xs)
162− | (G' ** xs') with (ReflectList (G' ++ G) ys)
159+%reflection
160+reflectEq : (a : Type) -> (G : List (List a)) -> (P : Type) -> (G' ** ListEq (G' ++ G) P)
161+reflectEq a G (the (List a) xs = the (List a) ys) with (reflectList G xs)
162+ | (G' ** xs') with (reflectList (G' ++ G) ys)
163163 | (G'' ** ys') = ((G'' ++ G') **
164164 rewrite (sym (appendAssociative G'' G' G)) in
165165 EqP (weaken G'' xs') ys')
@@ -196,14 +196,14 @@ Reflect.bp1 = proof {
196196
197197-- "quoteGoal x by p in e" does some magic
198198-- The effect is to bind x to p applied to the current goal. If 'p' is a
199−-- Reflection function (which is the most likely thing to be useful...)
199+-- reflection function (which is the most likely thing to be useful...)
200200-- then we can feed the result to the above 'prove' function and pull out
201201-- the proof, if it exists.
202202
203203-- The syntax declaration below just gives us an easy way to invoke the
204204-- prover.
205205
206−syntax AssocProof [ty] = quoteGoal x by ReflectEq ty [] in
206+syntax AssocProof [ty] = quoteGoal x by reflectEq ty [] in
207207 getJust (prove (getProof x)) ItIsJust
208208
209209