fix: re-add PFin2.elim0 (#6)

Co-authored-by: monsterkrampe <[email protected]>
alexkeizer · Feb 20, 2024 · 801eee8 · 801eee8
1 parent 7e50897
commit 801eee8
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/Qpf/MathlibPort/Fin2.lean b/Qpf/MathlibPort/Fin2.lean
@@ -46,6 +46,10 @@ inductive PFin2 : Nat → Type u
 
 namespace PFin2
 
+/-- Ex falso. The dependent eliminator for the empty `PFin2 0` type. -/
+def elim0 {C : PFin2 0 → Sort u} : ∀ i : PFin2 0, C i :=
+  by intro i; cases i
+
 /-- Converts a `PFin2` into a natural. -/
 def toNat : ∀ {n}, PFin2 n → Nat
   | _, @fz _ => 0