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

Replace example with something non-silly #21

Open jonsterling opened 7 years ago

jonsterling commented 7 years ago

The example demonstrates dependency, but in a silly / confusing way. Should replace this with something like a refiner for first order logic, or a little dependent type theory.