A smaller core with Pi/Sigma & macros

wilbowma / cur

A less devious proof assistant

BSD 2-Clause "Simplified" License

222 stars 18 forks source link

A smaller core with Pi/Sigma & macros #12

Closed wilbowma closed 6 years ago

wilbowma commented 9 years ago

The Gentle art of levitations Chapman et al. 2010, See also McBride et al. 2004, Transpprting functions across ornaments Dagand & McBride ICFP 2012, dybjer talk OPLSS 2015

wilbowma commented 6 years ago

Declaring this a non-goal. Cur is about extensibility. With the new Turnstile core, we want a small core, and then to add features (including type rules) via libraries.