A tiny language for teaching and experimenting with refinement types, in the style of LiquidHaskell.
- BUILD initial code
- STEAL make grammar more Haskelly
- PARSE in all Nano tests (but using Garter representation)
- PORT all the garter tests (using Haskelly syntax)
- PRINT all inferred (top-level) types
- ADD elaboration @a @b etc.
- PRINT "elaborated" expressions
- TYPE refinement type constraints
- GEN refinement type constraints
- SOLVE refinement type constraints (with fixpoint)
Language.Mist.Utils.MiscLanguage.Mist.Utils.UXLanguage.Mist.Utils.TestLanguage.Mist.Basic.TypesLanguage.Mist.Basic.ANFLanguage.Mist.Basic.WellFormedLanguage.Mist.Basic.CheckLanguage.Mist.Liquid.TypesLanguage.Mist.Liquid.Check