-
Notifications
You must be signed in to change notification settings - Fork 19
Open
Description
COQC solutions/SsrStyle_solutions.v
File "./solutions/SsrStyle_solutions.v", line 170, characters 0-90:
Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints]
= true
: bool
= false
: bool
And indeed gorgeous_b is defined using Fixpoint vernacular but it's not recursive:
Fixpoint gorgeous_b n : bool := match n with
| 1 | 2 | 4 | 7 => false
| _ => true
end.A quick search did not reveal if this was intentional, so feel free to close.
Metadata
Metadata
Assignees
Labels
No labels