Skip to content

Commit 0e999ee

Browse files
author
Alex Gryzlov
committed
fix Tactics
1 parent 894fb1f commit 0e999ee

File tree

1 file changed

+2
-2
lines changed

1 file changed

+2
-2
lines changed

src/Tactics.lidr

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -134,8 +134,8 @@ To use the \idr{exact} tactic, the (conclusion of the) fact being applied must
134134
match the goal exactly -- for example, \idr{exact} will not work if the left and
135135
right sides of the equality are swapped.
136136

137-
> silly3_firsttry : (n : Nat) -> True = beq_nat n 5 ->
138-
> beq_nat (S (S n)) 7 = True
137+
> silly3_firsttry : (n : Nat) -> True = n == 5 ->
138+
> (S (S n)) == 7 = True
139139
> silly3_firsttry = %runElab silly3_firsttry_tac
140140
> where
141141
> silly3_firsttry_tac : Elab ()

0 commit comments

Comments
 (0)