7490c34b54
- Delayed assignments do not become regular assignments anymore. - We can instantiate mvas more aggressively in the new design.
10 lines
387 B
Text
10 lines
387 B
Text
"[n.1, n.2, n.3, m1, m2, m3]"
|
||
"[(m1, ?n.1 α), (m2, ?n.3 α x), (m3, ?n.2 α x)]"
|
||
fun (α : Type) (x : ?n.1 α) (y : Nat -> (?n.3 α x)) => f (?n.2 α x) x
|
||
|
||
"[n.1, n.2, n.3, m1, m2, m3]"
|
||
"[(m1, ?n.1 α), (m2, ?n.3 α x)]"
|
||
"[n.2]"
|
||
fun (α : Type) (x : ?n.1 α) (y : Nat -> (?n.3 α x)) => f (?n.2 α x) y
|
||
assigning ?m1 and ?n.1
|
||
fun (α : Type) (x : Nat) (y : Nat -> (?n.3 α x)) => f x y
|