blob: f1dcae9773c17f42f3d721ca9a2dc426c2953123 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Require Import FunInd.
Set Universe Polymorphism.
Set Primitive Projections.
Set Implicit Arguments.
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 *)
|
