... | ... | @@ -170,7 +170,7 @@ V1 :: [a/alpha]Q1, ..., Vn :: [a/alpha]Qn |
|
|
```
|
|
|
|
|
|
|
|
|
The case \[IOCan3\] is the most complex one: we need to generate a function from the evidence generated by an implication. Such an implication generates a series of bindings, which we denote here using `[ ]`. Note that we abstract by values, types and constraints, but this is OK, because it is a System FC term.
|
|
|
The case \[IOCan3\] is the most complex one: we need to generate a function from the evidence generated by an implication. Such an implication generates a series of bindings, which we denote here using `[]`. Note that we abstract by values, types and constraints, but this is OK, because it is a System FC term.
|
|
|
|
|
|
```wiki
|
|
|
W1 :: InstanceOf sigma2 (forall a. Q1 => tau1)
|
... | ... | @@ -178,7 +178,7 @@ W1 :: InstanceOf sigma2 (forall a. Q1 => tau1) |
|
|
---->
|
|
|
|
|
|
W1 :: sigma2 -> (forall a. Q1 => tau1)
|
|
|
W1 = \x -> /\a -> \(d : Q1) -> let [ ] in (W2 x)
|
|
|
W1 = \x -> /\a -> \(d : Q1) -> let [] in (W2 x)
|
|
|
|
|
|
W2 :: forall a. (d : Q1) => (W2 :: InstanceOf sigma2 tau1)
|
|
|
```
|
... | ... | |