blob: 1cdb39b020c7934362e9404a78b80c8683ae528a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
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)
Arguments a (_ _)%type_scope _
b =
fun A : Type => let B := A in fun (C : Type) (u : U A C) => b _ _ u
: forall A : Type,
let B := A in
forall (C : Type) (u : U A C), (A, B, C, c _ _ u) = (A, B, C, c _ _ u)
Arguments b (_ _)%type_scope _
|
