Eliminating Dependent Pattern Matching
From MaRDI portal
Publication:5757920
DOI10.1007/11780274_27zbMath1132.68327OpenAlexW2113232207MaRDI QIDQ5757920
Conor McBride, Healfdene Goguen, James McKinna
Publication date: 7 September 2007
Published in: Algebra, Meaning, and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/11780274_27
Related Items
The Lean Theorem Prover (System Description) ⋮ Homotopy type theory in Lean ⋮ Elaborating dependent (co)pattern matching: No pattern left behind ⋮ Eliminating dependent pattern matching without K ⋮ Programming with ornaments ⋮ The calculus of dependent lambda eliminations ⋮ Partiality and recursion in interactive theorem provers – an overview ⋮ A New Elimination Rule for the Calculus of Inductive Constructions ⋮ Algebra of programming in Agda: Dependent types for relational program derivation
