Record the list of variables with their types in typing rules ?

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting

Other

280 stars 35 forks source link

Record the list of variables with their types in typing rules ? #168

Open fblanqui opened 5 years ago

fblanqui commented 5 years ago

This field would be set after checking subjection reduction. This would simplify termination and confluence checking. Note that it is important that termination and confluence checking is fast. Otherwise people won't use it.

rlepigre commented 5 years ago

Note that this is going to be very tricky, and it is not even clear what the type of a pattern variable is. Or is it? What about constraints for example?