LiFtEr: the `pred` field.

data61 / PSL

Other

64 stars 9 forks source link

Open yutakang opened 5 years ago

yutakang commented 5 years ago

Maybe LiFtEr should support pred. But this field is rarely used. So, this issue has a really low priority.

yutakang commented 5 years ago

An example would be line 193 in Applicative_Lifting/Idiomatic_Terms.thy.