diff options
Diffstat (limited to 'spec')
| -rw-r--r-- | spec/inferred.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/spec/inferred.md b/spec/inferred.md index 73fc4abd..ee899f5d 100644 --- a/spec/inferred.md +++ b/spec/inferred.md @@ -174,7 +174,7 @@ Let `vβπ¨π½βπΎπ©`, so that `vβ‘πΎz`. `v` is of course well-define - *Structural* Under: If `πΎ` is a structural function (to be defined below) and `v` is compatible with `πΎ` on `π©`, then the result is obtained by inserting `v` back into `π©`. - *Computational* Under: If `πΎ` is provably not a structural function, then the result is `πΎβΌv` if it is defined. -When implementing, there is no need to implement invertable Under specially: it can be handled as part of the structural and computation cases. +When implementing, there is no need to implement invertible Under specially: it can be handled as part of the structural and computation cases. ### Mathematical definition of structural Under |