a warning (or error?) if a bound variable captures something present in the environment ?

latte-central / LaTTe

LaTTe : a Laboratory for Type Theory experiments (in clojure)

http://latte-central.github.io/LaTTe/

MIT License

256 stars 13 forks source link

Closed fredokun closed 7 years ago

fredokun commented 8 years ago

if a variable e.g. x is in the environment

then something of the form (lambda [x T] ...) will possibly interfere with expressions having x as a free variable.

fredokun commented 7 years ago

I cannot reproduce this error, and many things have been modified in the kernel since I observed this one. So I close the issue for now.