fun S : store => S.(store_funcs)
: store -> host_func
a =
fun A : Type =>
let B := A in fun (C : Type) (u : U A C) => (A, B, C, c _ _ u)
: forall A : Type,
let B := A in
forall C : Type, U A C -> Type * Type * Type * (B * A * C)
a is a projection of U
Arguments a (A C)%_type_scope u
Record U (A : Type) (B : Type := A) (C : Type) : Type := Build_U
{ c : (B * A * C)%type; a := (A, B, C, c); b : a = a }.
U has primitive projections with eta conversion.
Arguments U (A C)%_type_scope
Arguments Build_U (A C)%_type_scope c b
Arguments c (A C)%_type_scope u
Arguments a (A C)%_type_scope u
Arguments b (A C)%_type_scope u
[ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
]
