Set Universe Polymorphism. Set Primitive Projections. SetImplicitArguments. Set Strongly Strict Implicit.
Function first_false (n : nat) (f : nat -> bool) : option nat := match n with
| O => None
| S m => match first_false m f with
| (Some _) as s => s
| None => if f m then None else Some m end end. (* undefined universe *)
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
