Skip to content

Commit c115d99

Browse files
committed
Tactics.sillyfun_false: add missing clauses to prove totality
1 parent 5ee3397 commit c115d99

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

src/Tactics.lidr

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -978,8 +978,10 @@ Here are some examples:
978978
> sillyfun_false : (n : Nat) -> sillyfun n = False
979979
> sillyfun_false n with (beq_nat n 3)
980980
> sillyfun_false (S (S (S Z))) | True = Refl
981+
> sillyfun_false n | True = Refl
981982
> sillyfun_false n | False with (beq_nat n 5)
982983
> sillyfun_false (S (S (S (S (S Z))))) | False | True = Refl
984+
> sillyfun_false n | False | True = Refl
983985
> sillyfun_false n | False | False = Refl
984986
985987

0 commit comments

Comments
 (0)