cedille.github.io

Language Overview

Please see the example programs below for a quick tour of some of Cedille’s important features.

• cov-pattern-matching.ced
• datatypes.ced
• equational-reasoning.ced
• implicit-products.ced
• induction-for-church-nats.ced
• local-definitions.ced
• obviously-false-equations.ced
• opaque-definitions.ced
• structural-operations.ced
• type-inference.ced
• type-quantification.ced