search

RedPRL / sml-dependent-lcf

A library for the next generation of LCF refiners, with support for dependent refinement—Long Live the Anti-Realist Struggle!
16 stars 1 forks source link

Delete generic judgment stuff #25

Closed jonsterling closed 7 years ago

jonsterling commented 7 years ago

I'm pretty sure that what I implemented is just incorrect, and I'm not sure how to fix it, so I'm deleting it. It's not too hard in practice to do generic judgment manually.