2
fun (P : t -> Type) (f : let x := t in forall x0 : x, P x0 -> P (k x0)) =>
4
match t as t0 return (P t0) with
5
| k _ x0 => f x0 (F x0)
7
: forall P : t -> Type,
8
(let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
10
fun (x y : nat) (P : nat -> Type) (def : P x) (prf : P y) =>
11
match eq_nat_dec x y with
13
match eqprf in (_ = z) return (P z) with
18
: forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
20
Argument scopes are [nat_scope nat_scope _ _ _]
22
fix foo (A : Type) (l : list A) {struct l} : option A :=
25
| x0 :: nil => Some x0
26
| x0 :: (_ :: _) as l0 => foo A l0
28
: forall A : Type, list A -> option A
30
Argument scopes are [type_scope list_scope]
31
foo' = if A 0 then true else false