eqT_rect@{u u0} =
fun (A : Type@{u}) (a : A) (P : forall a0 : A, eqT@{u} a a0 -> Type@{u0})
(f : P a (reflT@{u} a)) (a0 : A) (e : eqT@{u} a a0) =>
match e :> eqT@{u} a _ as e0 in (eqT _ a1) return (P a1 e0) with
| reflT _ => f
end
: forall (A : Type@{u}) (a : A)
(P : forall a0 : A, eqT@{u} a a0 -> Type@{u0}),
P a (reflT@{u} a) -> forall (a0 : A) (e : eqT@{u} a a0), P a0 e
(* u u0 |= *)
Arguments eqT_rect A%_type_scope a P%_function_scope f a0 e
seq_rect =
fun (A : Type@{seq_rect.u1}) (a : A)
(P : forall a0 : A, seq a a0 -> Type@{seq_rect.u0})
(f : P a (srefl a)) (a0 : A) (s : seq a a0) =>
match s :> seq a a0 as s0 in (seq _ a1) return (P a1 s0) with
| srefl _ => f
end
: forall (A : Type@{seq_rect.u1}) (a : A)
(P : forall a0 : A, seq a a0 -> Type@{seq_rect.u0}),
P a (srefl a) -> forall (a0 : A) (s : seq a a0), P a0 s
Arguments seq_rect A%_type_scope a P%_function_scope f a0 s
eq_sym =
fun (A : Type) (x y : A) (H : @eq A x y) =>
match H in (@eq _ _ a) return (@eq A a x) with
| @eq_refl _ _ => @eq_refl A x
end
: forall [A : Type] [x y : A] (_ : @eq A x y), @eq A y x
Arguments eq_sym [A]%_type_scope [x y] _
eq_sym =
fun (A : Type) (x y : A) (H : x = y) =>
match H in (_ = a) return (a = x) with
| @eq_refl _ _ => @eq_refl A x
end
: forall [A : Type] [x y : A], x = y -> y = x
Arguments eq_sym [A]%_type_scope [x y] _
eq_sym =
fun (A : Type) (x y : A) (H : x = y) =>
match H in (_ = a) return (a = x) with
| @eq_refl _ _ => @eq_refl A x
end
: forall [A : Type] [x y : A], x = y -> y = x
Arguments eq_sym [A]%_type_scope [x y] _
test =
fun (O : unit) (S : nat -> unit) (n : nat) =>
match n with
| 0 => O
| Datatypes.S n0 => S n0
end
: unit -> (nat -> unit) -> nat -> unit
Arguments test O S%_function_scope n%_nat_scope
[ Dauer der Verarbeitung: 0.20 Sekunden
(vorverarbeitet)
]
