search

data61 / PSL

Other
65 stars 9 forks source link

SeLFiE: assertions for types #150

Open yutakang opened 4 years ago

yutakang commented 4 years ago

We should be able to check the type of a term (/ term occurrence). For now it suffices to check if the type is one of the following:

yutakang commented 3 years ago

Maybe detecting function types would be good when proof goals have variables that are functions.