@@ -19,15 +19,15 @@ plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
1919plusZeroRightNeutralNew Z = Refl
2020plusZeroRightNeutralNew (S k) =
2121 %runElab (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
22− fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
23− solve)
22+ fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
23+ solve)
2424
2525plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
2626plusSuccRightSuccNew Z k = Refl
2727plusSuccRightSuccNew (S j) k =
2828 %runElab (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
29− fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
30− solve)
29+ fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
30+ solve)
3131
3232-- Test that side effects in new tactics work
3333
@@ -35,7 +35,7 @@ mkDecl : ()
3535mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
3636 [Implicit (UN "z") `(Nat)]
3737 `(Vect ~(Var (UN "z")) ())
38− fill `(() : ())
39− solve)
38+ fill `(() : ())
39+ solve)
4040
4141repUnit = pure ()