Language

Package: cedille @ 1.1.2

Synopsis

Language based on Calculus of Dependent Lambda Eliminations

Description

Cedille is an interactive theorem-prover and dependently typed programming language, based on extrinsic (aka Curry-style) type theory. This makes it rather different from type theories like Coq and Agda, which are intrinsic (aka Church-style). In Cedille, terms are nothing more than annotated versions of terms of pure untyped lambda calculus. In contrast, in Coq or Agda, the typing annotations are intrinsic parts of terms. The typing annotations can only be erased as an optimization under certain conditions, not by virtue of the definition of the type theory.

Home page
https://cedille.github.io/
Location
gnu/packages/cedille.scm (line: 31, column: 2)
License

Lint warnings

LinterMessageLocation
optional-tests

Make sure tests are only run when requested

the 'check' phase should respect #:tests?
optional-tests

Make sure tests are only run when requested

the 'check' phase should respect #:tests?