Skip to content

Commit 2d4f1e6

Browse files
committed
Tactics: remove superfluous sillyfun_false clauses
1 parent 3844d70 commit 2d4f1e6

File tree

1 file changed

+0
-2
lines changed

1 file changed

+0
-2
lines changed

src/Tactics.lidr

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -971,10 +971,8 @@ Here are some examples:
971971
972972
> sillyfun_false : (n : Nat) -> sillyfun n = False
973973
> sillyfun_false n with (beq_nat n 3)
974-
> sillyfun_false (S (S (S Z))) | True = Refl
975974
> sillyfun_false n | True = Refl
976975
> sillyfun_false n | False with (beq_nat n 5)
977-
> sillyfun_false (S (S (S (S (S Z))))) | False | True = Refl
978976
> sillyfun_false n | False | True = Refl
979977
> sillyfun_false n | False | False = Refl
980978

0 commit comments

Comments
 (0)