We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 7b4c9b7 commit adda267Copy full SHA for adda267
docs/docs/reference/metaprogramming/simple-smp.md
@@ -123,7 +123,7 @@ Proof by structural induction over terms.
123
124
To prove (1):
125
126
- - the cases for variables, lambdas and applications are as in [STL](https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus).
+ - the cases for variables, lambdas and applications are as in [STLC](https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus).
127
- If `t = ’t2`, then by inversion we have ` ’ E1 |- t2: T2` for some type `T2`.
128
By the second [induction hypothesis](https://en.wikipedia.org/wiki/Mathematical_induction) (I.H.), we have one of:
129
- `t2 = u`, hence `’t2` is a value,
0 commit comments