Eliminating dependent pattern matching without K (Q5371975): Difference between revisions

@@ Property / cites work @@
+A New Elimination Rule for the Calculus of Inductive Constructions
+Normal rank
@@ Property / cites work @@
+Q2968413
@@ Property / cites work: Q2968413 / rank @@
+Normal rank
@@ Property / cites work @@
+Idris, a general-purpose dependently typed programming language: Design and implementation
+Normal rank
@@ Property / cites work @@
+Pattern matching without K
@@ Property / cites work: Pattern matching without K / rank @@
+Normal rank
@@ Property / cites work @@
+Unifiers as equivalences: proof-relevant unification of dependently typed data
+Normal rank
@@ Property / cites work @@
+The Lean Theorem Prover (System Description)
@@ Property / cites work: The Lean Theorem Prover (System Description) / rank @@
+Normal rank
@@ Property / cites work @@
+On the bright side of type classes
@@ Property / cites work: On the bright side of type classes / rank @@
+Normal rank
@@ Property / cites work @@
+Eliminating Dependent Pattern Matching
@@ Property / cites work: Eliminating Dependent Pattern Matching / rank @@
+Normal rank
@@ Property / cites work @@
+Generalizations of Hedberg’s Theorem
@@ Property / cites work: Generalizations of Hedberg’s Theorem / rank @@
+Normal rank
@@ Property / cites work @@
+Higher Homotopies in a Hierarchy of Univalent Universes
+Normal rank
@@ Property / cites work @@
+Calculating the Fundamental Group of the Circle in Homotopy Type Theory
+Normal rank
@@ Property / cites work @@
+Q4296744
@@ Property / cites work: Q4296744 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4736399
@@ Property / cites work: Q4736399 / rank @@
+Normal rank
@@ Property / cites work @@
+Advanced Functional Programming
@@ Property / cites work: Advanced Functional Programming / rank @@
+Normal rank
@@ Property / cites work @@
+The view from the left
@@ Property / cites work: The view from the left / rank @@
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Q4281483
@@ Property / cites work: Q4281483 / rank @@
+Normal rank
@@ Property / cites work @@
+Equations: A Dependent Pattern-Matching Compiler
@@ Property / cites work: Equations: A Dependent Pattern-Matching Compiler / rank @@
+Normal rank
@@ Property / cites work @@
+The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013, vii + 583 pp.
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1017/s0956796816000174
+Normal rank
@@ Property / OpenAlex ID @@
+W2516238737
@@ Property / OpenAlex ID: W2516238737 / rank @@
+Normal rank