... | ... | @@ -153,7 +153,9 @@ Int :: Int :=: Int |
|
|
Coercion variables are
|
|
|
used to abstract over evidence of type equality, as in
|
|
|
|
|
|
> `(/\c::(a :=: Bool). \x::a. if (x `cast` c) then 0 else 1) :: (a :=: Bool) => a -> Int`
|
|
|
```wiki
|
|
|
(/\c::(a :=: Bool). \x::a. if (x `cast` c) then 0 else 1) :: (a :=: Bool) => a -> Int
|
|
|
```
|
|
|
|
|
|
|
|
|
There are also coercion constants that are introduced by the compiler
|
... | ... | |