Cedille Versions Save

Cedille, a dependently typed programming languages based on the Calculus of Dependent Lambda Eliminations

v1.1.2

4 years ago
  • add support for MacOS install paths for package managers like brew
  • add stack configuration for building from source with stack
  • improve MacOS App Bundle support

v1.1.1

5 years ago

Cedille 1.1.1

  • support for simple inference of motives for pattern matches. This probably should have been 1.1, but we are releasing it now. It is demo'ed in the language-overview/datatypes.ced file.
  • Cedille Core checker now uses de Bruijn indices for bound variables, and runs quite a bit faster now.
  • you no longer need to parenthesize mu and mu' expressions if you are applying them to arguments.

v1.1.0

5 years ago

Cedille 1.1

  • support for datatype notations. See language-overview/datatypes.ced and language-overview/cov-pattern-matching.ced. Please note that "data" and "close" are now keywords and cannot be used as identifiers in Cedille code.
  • elaboration to Cedille Core with keystroke "E", and checking of generated .cdle files from within emacs using the Cedille Core checker.
  • colon is now allowed instead of left triangle for classifications.
  • better support for implicit arguments with let-terms; see language-overview/local-definitions.ced.
  • reversed the direction of rewriting for synthesizing rhos, for the benefit of checking in Cedille Core
  • various bug fixes

v1.0.0

5 years ago

This is the version 1.0.0 releases of Cedille. The attached Debian package will get Cedille installed without the need to install a lot of other software (Haskell, Agda, the Iowa Agda Library, etc.). If you do want to build from sources, clone the repo and consult the INSTALL.txt file.

The Debian package does not come with any sample .ced files. You can see some if you clone the repo and look at language-overview/ or lib/.

There is a MacOS dmg file available now as well.