Elaborating dependent (co)pattern matching: No pattern left behind (Q5110925): Difference between revisions

@@ Property / cites work @@
+Wellfounded recursion with copatterns
@@ Property / cites work: Wellfounded recursion with copatterns / rank @@
+Normal rank
@@ Property / cites work @@
+Copatterns
@@ Property / cites work: Copatterns / rank @@
+Normal rank
@@ Property / cites work @@
+Logic Programming with Focusing Proofs in Linear Logic
+Normal rank
@@ Property / cites work @@
+Friends with Benefits
@@ Property / cites work: Friends with Benefits / rank @@
+Normal rank
@@ Property / cites work @@
+Idris, a general-purpose dependently typed programming language: Design and implementation
+Normal rank
@@ Property / cites work @@
+Types for Proofs and Programs
@@ Property / cites work: Types for Proofs and Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Unifiers as equivalences: proof-relevant unification of dependently typed data
+Normal rank
@@ Property / cites work @@
+Telescopic mappings in typed lambda calculus
@@ Property / cites work: Telescopic mappings in typed lambda calculus / rank @@
+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 @@
+Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
+Normal rank
@@ Property / cites work @@
+Eliminating Dependent Pattern Matching
@@ Property / cites work: Eliminating Dependent Pattern Matching / rank @@
+Normal rank
@@ Property / cites work @@
+Focusing on pattern matching
@@ Property / cites work: Focusing on pattern matching / 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 @@
+Q4247309
@@ Property / cites work: Q4247309 / rank @@
+Normal rank
@@ Property / cites work @@
+Unnesting of Copatterns
@@ Property / cites work: Unnesting of Copatterns / 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 @@
+Indexed codata types
@@ Property / cites work: Indexed codata types / rank @@
+Normal rank
@@ Property / cites work @@
+Focusing and higher-order abstract syntax
@@ Property / cites work: Focusing and higher-order abstract syntax / rank @@
+Normal rank