search

latte-central / latte-kernel

The (very) small kernel of the LaTTe proof assistant
MIT License
11 stars 4 forks source link

partially apply references #28

Closed fredokun closed 3 years ago

fredokun commented 3 years ago

Suppose f is a reference expecting one argument. There is an ambiguity between (f y) i.e. passing argument y to f and [f y] applying term f to term y. Both are normal forms but only the former should be

fredokun commented 3 years ago

This has been implemented in commit https://github.com/latte-central/latte-kernel/commit/e323e2ec4445a36578c3d2d1af2aed78d995887d