ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-13 07:26:59 +03:00
Code Issues Projects Releases Wiki Activity

Update indentation in test

Browse Source
This commit is contained in:
David Raymond Christiansen 2015-04-15 12:15:56 +02:00
parent 367c037e4b
commit 6c7c8870b2
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
test/tactics001/Tactics.idr
View File

@ -19,15 +19,15 @@ plusZeroRightNeutralNew : (n : Nat) -> plus n 0 = n
plusZeroRightNeutralNew Z = Refl
plusZeroRightNeutralNew (S k) =
%runElab (do rewriteWith `(sym $ plusZeroRightNeutralNew ~(Var "k"))
fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
solve)
fill $ refl `(Nat : Type) `(S ~(Var (UN "k")))
solve)
plusSuccRightSuccNew : (j, k : Nat) -> plus j (S k) = S (plus j k)
plusSuccRightSuccNew Z k = Refl
plusSuccRightSuccNew (S j) k =
%runElab (do rewriteWith `(sym $ plusSuccRightSuccNew ~(Var "j") ~(Var (UN "k")))
fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
solve)
fill $ refl `(Nat : Type) `(S (S (plus ~(Var (UN "j")) ~(Var (UN "k")))))
solve)
-- Test that side effects in new tactics work
@ -35,7 +35,7 @@ mkDecl : ()
mkDecl = %runElab (do declareType $ Declare (NS (UN "repUnit") ["Tactics"])
[Implicit (UN "z") `(Nat)]
`(Vect ~(Var (UN "z")) ())
fill `(() : ())
solve)
fill `(() : ())
solve)
repUnit = pure ()