Performance issues when pattern matching

Stream: lean4

[Chris Hughes]

In the following code, function1 causes no problems, but the unfinished function2 causes a deterministic timeout. I think this is just because Lean is trying to print too many missing cases. A missing case looks something like this T.mk2 (Data.mk true true true true true true) (Data.mk true true true true true true), so there are I think 32768 missing cases it is trying to print.

structure Data : Type :=
( A : Bool )
( B : Bool )
( C : Bool )
( D : Bool )
( E : Bool )
( F : Bool )

inductive T : Type
| mk1 (d₁ d₂ : Data) : T
| mk2 (d₁ d₂ : Data) : T
| mk3 (d₁ d₂ : Data) : T
| mk4 (d₁ d₂ : Data) : T
| mk5 (d₁ d₂ : Data) : T
| mk6 (d₁ d₂ : Data) : T
| mk7 (d₁ d₂ : Data) : T
| mk8 (d₁ d₂ : Data) : T
| mk9 (d₁ d₂ : Data) : T

def function1 : (x : T) → Nat
| T.mk1 _ _ => 0
| T.mk2 _ _ => 0
| T.mk3 _ _ => 0
| T.mk4 _ _ => 0
| T.mk5 _ _ => 0
| T.mk6 _ _ => 0
| T.mk7 _ _ => 0
| T.mk8 _ _ => 0
| T.mk9 _ _ => 0

def function2 : (x : T) → Nat
| T.mk1 _ _ => _