empty type

Stream: mathlib4

[Heather Macbeth]

I am trying to port data.fin.fin2 and came up with the following tactic proof involving an empty type; what would be the term version?

open Nat

inductive Fin2 : ℕ → Type
  |
  /-- `0` as a member of `fin (succ n)` (`fin 0` is empty) -/
  fz {n} : Fin2 (succ n)
  |
  /-- `n` as a member of `fin (succ n)` -/
  fs {n} : Fin2 n → Fin2 (succ n)

def elim0 {C : Fin2 0 → Sort u} : ∀ i : Fin2 0, C i :=
  fun i => by cases i

In Lean 3 it is

def elim0 {C : fin2 0 → Sort u} : Π (i : fin2 0), C i.

[Jannis Limperg]

def elim0 {C : Fin2 0 → Sort u} : ∀ i : Fin2 0, C i :=
  fun i => nomatch i

[Mario Carneiro]

import Std.Tactic.NoMatch

def elim0 {C : Fin2 0 → Sort u} : ∀ i : Fin2 0, C i := fun.

is the equivalent of the lean 3 syntax

[Mario Carneiro]

it acts similar to fun i => nomatch i, except it will introduce all arguments and look for empty pattern matches on all of them.

[Heather Macbeth]

Aha, thank you both. Mathport had correctly produced Mario's version, but it didn't have the import.

[Heather Macbeth]

So presumably this issue will go away as we move up the hierarchy.

[Mario Carneiro]

Yes, if mathport ever produces a syntax that doesn't work, try to find the import that makes it work rather than stubbing it out (unless that import is Mathlib.Mathport.Syntax since those syntaxes haven't been implemented yet)

[Mario Carneiro]

Mathport cheats by using import Mathlib itself