ilyasergey / pnp

Lecture notes for a short course on proving/programming in Coq via SSReflect.
https://ilyasergey.net/pnp
BSD 2-Clause "Simplified" License
159 stars 16 forks source link

non-recursive fixpoint warning #24

Open anton-trunov opened 3 years ago

anton-trunov commented 3 years ago
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.