max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

perf: isClassQuick? was incorrectly producing undef

Browse source 
Then `isClassExpensive?` was being invoked too often. In some
benchmarks the performance hit was substantial. For example,
in the new test `state8.lean`. The runtime on my machine went from 2s
to 0.76s.
This commit is contained in:
Leonardo de Moura 2022-04-09 10:32:13 -07:00
parent 6e02514eee
commit 7d99f6f555
7 changed files with 211 additions and 140 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Meta/Basic.lean
View file

@ -593,8 +593,8 @@ private def isClassQuickConst? (constName : Name) : MetaM (LOption Name) := do
pure (LOption.some constName)
else
match (← getConstTemp? constName) with
| some _ => pure LOption.undef
| none => pure LOption.none
| some (ConstantInfo.defnInfo ..) => pure LOption.undef -- We may be able to unfold the definition
| _ => pure LOption.none
private partial def isClassQuick? : Expr → MetaM (LOption Name)
| Expr.bvar .. => pure LOption.none

12
tests/lean/1018unknowMVarIssue.lean.expected.out
View file

@ -7,15 +7,15 @@ a : α
⊢ α
[Elab.info] command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
[.] `α : some Sort.{?_uniq.313} @ ⟨7, 13⟩-⟨7, 14⟩
[.] `α : some Sort.{?_uniq.311} @ ⟨7, 13⟩-⟨7, 14⟩
α : Type @ ⟨7, 13⟩-⟨7, 14⟩
a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
[.] `α : some Sort.{?_uniq.319} @ ⟨7, 13⟩-⟨7, 14⟩
[.] `α : some Sort.{?_uniq.317} @ ⟨7, 13⟩-⟨7, 14⟩
α : Type @ ⟨7, 13⟩-⟨7, 14⟩
a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
[.] `Fam2 : some Sort.{?_uniq.321} @ ⟨7, 21⟩-⟨7, 25⟩
[.] `Fam2 : some Sort.{?_uniq.319} @ ⟨7, 21⟩-⟨7, 25⟩
Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
[.] `α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
@ -25,7 +25,7 @@ a : α
β : Type @ ⟨7, 28⟩-⟨7, 29⟩
x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
[.] `β : some Sort.{?_uniq.323} @ ⟨7, 33⟩-⟨7, 34⟩
[.] `β : some Sort.{?_uniq.321} @ ⟨7, 33⟩-⟨7, 34⟩
β : Type @ ⟨7, 33⟩-⟨7, 34⟩
_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
@ -45,7 +45,7 @@ a : α
[.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
@Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
[.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.654]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.655]]]) @ ⟨9, 4⟩-⟨9, 12⟩
[.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.652]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.653]]]) @ ⟨9, 4⟩-⟨9, 12⟩
α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
@ -56,7 +56,7 @@ a : α
Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
[.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
a : α @ ⟨8, 2⟩†-⟨10, 19⟩†
[.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.686]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.687]]]) @ ⟨10, 4⟩-⟨10, 12⟩
[.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.684]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq.685]]]) @ ⟨10, 4⟩-⟨10, 12⟩
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
n : Nat @ ⟨10, 13⟩-⟨10, 14⟩

8
tests/lean/evalWithMVar.lean.expected.out
View file

@ -1,11 +1,11 @@
Sum.someRight c : Option Nat
evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument
@Sum.someRight ?m Nat c
context:
⊢ Type u_1
evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument
@c ?m
context:
⊢ Type u_1
evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument
@Sum.someRight ?m Nat c
context:
⊢ Type u_1
Sum.someRight c : Option Nat
Sum.someRight c : Option Nat

2
tests/lean/holes.lean.expected.out
View file

@ -22,12 +22,12 @@ x : Nat
⊢ Type
holes.lean:13:10-13:11: error: failed to infer binder type
holes.lean:15:16-15:17: error: failed to infer binder type
holes.lean:18:9-18:10: error: failed to infer binder type
holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument
@f Nat (?m a) a
context:
a : Nat
f : {α : Type} → {β : ?m a} → α → α := fun {α} {β} a => a
⊢ ?m a
holes.lean:18:9-18:10: error: failed to infer binder type
holes.lean:21:25-22:4: error: failed to infer definition type
holes.lean:25:8-25:11: error: failed to infer 'let rec' declaration type

134
tests/lean/infoTree.lean.expected.out
View file

@ -1,6 +1,6 @@
[Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩ @ Lean.Elab.Command.elabDeclaration
Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.422} @ ⟨13, 11⟩-⟨13, 14⟩
[.] `Nat : some Sort.{?_uniq.395} @ ⟨13, 11⟩-⟨13, 14⟩
Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
x (isBinder := true) : Nat @ ⟨13, 7⟩-⟨13, 8⟩
Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ «_aux_Init_Notation___macroRules_term_×__1»
@ -11,10 +11,10 @@
Nat × Nat : Type @ ⟨13, 18⟩†-⟨13, 27⟩ @ Lean.Elab.Term.elabApp
Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 27⟩†
Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Type.{?_uniq.426} @ ⟨13, 18⟩-⟨13, 21⟩
[.] `Nat : some Type.{?_uniq.399} @ ⟨13, 18⟩-⟨13, 21⟩
Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Type.{?_uniq.425} @ ⟨13, 24⟩-⟨13, 27⟩
[.] `Nat : some Type.{?_uniq.398} @ ⟨13, 24⟩-⟨13, 27⟩
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
f (isBinder := true) : Nat → Nat × Nat @ ⟨13, 4⟩-⟨13, 5⟩
x (isBinder := true) : Nat @ ⟨13, 7⟩-⟨13, 8⟩
@ -42,16 +42,16 @@
[Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩ @ Lean.Elab.Command.elabDeclaration
∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.455} @ ⟨17, 15⟩-⟨17, 18⟩
[.] `Nat : some Sort.{?_uniq.427} @ ⟨17, 15⟩-⟨17, 18⟩
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
x (isBinder := true) : Nat @ ⟨17, 9⟩-⟨17, 10⟩
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.457} @ ⟨17, 15⟩-⟨17, 18⟩
[.] `Nat : some Sort.{?_uniq.429} @ ⟨17, 15⟩-⟨17, 18⟩
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
y (isBinder := true) : Nat @ ⟨17, 11⟩-⟨17, 12⟩
Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow
Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ @ Lean.Elab.Term.elabIdent
[.] `Bool : some Sort.{?_uniq.460} @ ⟨17, 27⟩-⟨17, 31⟩
[.] `Bool : some Sort.{?_uniq.432} @ ⟨17, 27⟩-⟨17, 31⟩
Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
b (isBinder := true) : Bool @ ⟨17, 23⟩-⟨17, 24⟩
x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
@ -116,20 +116,20 @@
[Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ @ Lean.Elab.Command.elabDeclaration
Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.579} @ ⟨21, 16⟩-⟨21, 19⟩
[.] `Nat : some Sort.{?_uniq.548} @ ⟨21, 16⟩-⟨21, 19⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
x (isBinder := true) : Nat @ ⟨21, 10⟩-⟨21, 11⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.581} @ ⟨21, 16⟩-⟨21, 19⟩
[.] `Nat : some Sort.{?_uniq.550} @ ⟨21, 16⟩-⟨21, 19⟩
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
y (isBinder := true) : Nat @ ⟨21, 12⟩-⟨21, 13⟩
Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ @ Lean.Elab.Term.elabIdent
[.] `Bool : some Sort.{?_uniq.584} @ ⟨21, 28⟩-⟨21, 32⟩
[.] `Bool : some Sort.{?_uniq.553} @ ⟨21, 28⟩-⟨21, 32⟩
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
b (isBinder := true) : Bool @ ⟨21, 24⟩-⟨21, 25⟩
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.586} @ ⟨21, 36⟩-⟨21, 39⟩
[.] `Nat : some Sort.{?_uniq.555} @ ⟨21, 36⟩-⟨21, 39⟩
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
f2 (isBinder := true) : Nat → Nat → Bool → Nat @ ⟨21, 4⟩-⟨21, 6⟩
fun x y b =>
@ -253,10 +253,10 @@
Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩†
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Type.{?_uniq.797} @ ⟨27, 12⟩-⟨27, 15⟩
[.] `Nat : some Type.{?_uniq.763} @ ⟨27, 12⟩-⟨27, 15⟩
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
[.] `Array : some Type.{?_uniq.796} @ ⟨27, 18⟩-⟨27, 23⟩
[.] `Array : some Type.{?_uniq.762} @ ⟨27, 18⟩-⟨27, 23⟩
Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen
Macro expansion
@ -264,17 +264,17 @@
===>
Array Nat
Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp
[.] `Array : some Type.{?_uniq.798} @ ⟨27, 25⟩-⟨27, 30⟩
[.] `Array : some Type.{?_uniq.764} @ ⟨27, 25⟩-⟨27, 30⟩
Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Type.{?_uniq.799} @ ⟨27, 31⟩-⟨27, 34⟩
[.] `Nat : some Type.{?_uniq.765} @ ⟨27, 31⟩-⟨27, 34⟩
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp
[.] `Array : some Sort.{?_uniq.801} @ ⟨27, 39⟩-⟨27, 44⟩
[.] `Array : some Sort.{?_uniq.767} @ ⟨27, 39⟩-⟨27, 44⟩
Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Type.{?_uniq.802} @ ⟨27, 45⟩-⟨27, 48⟩
[.] `Nat : some Type.{?_uniq.768} @ ⟨27, 45⟩-⟨27, 48⟩
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩
s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
@ -291,11 +291,11 @@
f3 (isBinder := true) : Nat × Array (Array Nat) → Array Nat @ ⟨27, 4⟩-⟨27, 6⟩
[Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration
B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent
[.] `B : some Sort.{?_uniq.844} @ ⟨30, 14⟩-⟨30, 15⟩
[.] `B : some Sort.{?_uniq.809} @ ⟨30, 14⟩-⟨30, 15⟩
B : Type @ ⟨30, 14⟩-⟨30, 15⟩
arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.846} @ ⟨30, 19⟩-⟨30, 22⟩
[.] `Nat : some Sort.{?_uniq.811} @ ⟨30, 19⟩-⟨30, 22⟩
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
f4 (isBinder := true) : B → Nat @ ⟨30, 4⟩-⟨30, 6⟩
arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩
@ -311,11 +311,11 @@
f4 (isBinder := true) : B → Nat @ ⟨30, 4⟩-⟨30, 6⟩
[Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ @ Lean.Elab.Command.elabDeclaration
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.867} @ ⟨33, 12⟩-⟨33, 15⟩
[.] `Nat : some Sort.{?_uniq.831} @ ⟨33, 12⟩-⟨33, 15⟩
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩
B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent
[.] `B : some Sort.{?_uniq.869} @ ⟨33, 19⟩-⟨33, 20⟩
[.] `B : some Sort.{?_uniq.833} @ ⟨33, 19⟩-⟨33, 20⟩
B : Type @ ⟨33, 19⟩-⟨33, 20⟩
f5 (isBinder := true) : Nat → B @ ⟨33, 4⟩-⟨33, 6⟩
x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩
@ -356,77 +356,77 @@ infoTree.lean:44:0: error: expected stx
[.] (Command.set_option "set_option" `pp.raw) @ ⟨44, 0⟩-⟨44, 17⟩
[Elab.info] command @ ⟨45, 0⟩-⟨47, 8⟩ @ Lean.Elab.Command.elabDeclaration
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.891} @ ⟨45, 14⟩-⟨45, 17⟩
[.] `Nat : some Sort.{?_uniq.854} @ ⟨45, 14⟩-⟨45, 17⟩
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
_uniq.892 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
_uniq.855 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.893} @ ⟨45, 14⟩-⟨45, 17⟩
[.] `Nat : some Sort.{?_uniq.856} @ ⟨45, 14⟩-⟨45, 17⟩
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
_uniq.894 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
Eq.{1} Nat _uniq.892 _uniq.892 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
_uniq.857 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
Eq.{1} Nat _uniq.855 _uniq.855 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
Macro expansion
(«term_=_» `x "=" `x)
===>
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.179 `x `x)
Eq.{1} Nat _uniq.892 _uniq.892 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel
_uniq.892 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
Eq.{1} Nat _uniq.855 _uniq.855 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel
_uniq.855 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
[.] `x : none @ ⟨45, 21⟩-⟨45, 22⟩
_uniq.892 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
_uniq.892 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
_uniq.855 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
_uniq.855 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
[.] `x : none @ ⟨45, 25⟩-⟨45, 26⟩
_uniq.892 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
_uniq.898 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
_uniq.901 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
_uniq.902 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
(fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.901 _uniq.902]) f6.f7 : Eq.{1} Nat _uniq.901 _uniq.901 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
_uniq.855 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
_uniq.861 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
_uniq.862 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
_uniq.863 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
(fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.862 _uniq.863]) f6.f7 : Eq.{1} Nat _uniq.862 _uniq.862 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.903} @ ⟨46, 20⟩-⟨46, 23⟩
[.] `Nat : some Sort.{?_uniq.864} @ ⟨46, 20⟩-⟨46, 23⟩
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
_uniq.904 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
_uniq.865 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
[.] `Nat : some Sort.{?_uniq.905} @ ⟨46, 20⟩-⟨46, 23⟩
[.] `Nat : some Sort.{?_uniq.866} @ ⟨46, 20⟩-⟨46, 23⟩
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
_uniq.906 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.{1} Nat _uniq.904 _uniq.904 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
_uniq.867 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.{1} Nat _uniq.865 _uniq.865 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
Macro expansion
(«term_=_» `x "=" `x)
===>
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.187 `x `x)
Eq.{1} Nat _uniq.904 _uniq.904 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel
_uniq.904 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
_uniq.904 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
_uniq.904 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
_uniq.904 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
_uniq.911 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
_uniq.914 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
_uniq.915 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.refl.{1} Nat _uniq.914 : Eq.{1} Nat _uniq.914 _uniq.914 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
[.] `Eq.refl : some Eq.{?_uniq.908} Nat _uniq.914 _uniq.914 @ ⟨46, 36⟩-⟨46, 43⟩
Eq.{1} Nat _uniq.865 _uniq.865 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel
_uniq.865 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
_uniq.865 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
_uniq.865 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
_uniq.865 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
_uniq.872 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
_uniq.873 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
_uniq.874 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
Eq.refl.{1} Nat _uniq.873 : Eq.{1} Nat _uniq.873 _uniq.873 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
[.] `Eq.refl : some Eq.{?_uniq.869} Nat _uniq.873 _uniq.873 @ ⟨46, 36⟩-⟨46, 43⟩
Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩
_uniq.914 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
_uniq.914 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
[mdata _recApp: _uniq.911 _uniq.901 _uniq.902] : Eq.{1} Nat _uniq.901 _uniq.901 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
_uniq.911 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
_uniq.901 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
_uniq.901 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
_uniq.902 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
_uniq.902 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
_uniq.873 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
_uniq.873 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
[mdata _recApp: _uniq.872 _uniq.862 _uniq.863] : Eq.{1} Nat _uniq.862 _uniq.862 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
_uniq.872 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
_uniq.862 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
_uniq.862 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
_uniq.863 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
_uniq.863 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
f6.f7 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
f6 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨45, 4⟩-⟨45, 6⟩
[Elab.info] command @ ⟨50, 0⟩-⟨50, 32⟩ @ Lean.Elab.Command.elabDeclaration
B : Type @ ⟨50, 12⟩-⟨50, 13⟩ @ Lean.Elab.Term.elabIdent
[.] `B : some Sort.{?_uniq.939} @ ⟨50, 12⟩-⟨50, 13⟩
[.] `B : some Sort.{?_uniq.896} @ ⟨50, 12⟩-⟨50, 13⟩
B : Type @ ⟨50, 12⟩-⟨50, 13⟩
_uniq.940 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
_uniq.897 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent
[.] `B : some Sort.{?_uniq.941} @ ⟨50, 17⟩-⟨50, 18⟩
[.] `B : some Sort.{?_uniq.898} @ ⟨50, 17⟩-⟨50, 18⟩
B : Type @ ⟨50, 17⟩-⟨50, 18⟩
_uniq.942 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
_uniq.944 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
B.mk (B.pair _uniq.944) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
B.pair _uniq.944 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
_uniq.944 : B @ ⟨50, 24⟩-⟨50, 25⟩
[.] _uniq.944 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
_uniq.899 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
_uniq.900 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
B.mk (B.pair _uniq.900) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
B.pair _uniq.900 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
_uniq.900 : B @ ⟨50, 24⟩-⟨50, 25⟩
[.] _uniq.900 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
B.pair : B -> (Prod.{0 0} A A) @ ⟨50, 24⟩†-⟨50, 25⟩†
pair : Prod.{0 0} A A := B.pair _uniq.944 @ ⟨50, 22⟩†-⟨50, 32⟩
pair : Prod.{0 0} A A := B.pair _uniq.900 @ ⟨50, 22⟩†-⟨50, 32⟩
f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩

120
tests/lean/jason1.lean.expected.out
View file

@ -1,3 +1,35 @@
jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
@TySyntaxLayer.arrow G T EG getCtx
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
(@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
(@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
@ -12,6 +44,34 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
@ -62,63 +122,3 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:48:41-48:130: error: don't know how to synthesize implicit argument
@TySyntaxLayer.arrow G T EG getCtx
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))
(@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
(@EGrfl
(getCtx
(TAlgebra
(@TySyntaxLayer.nat G T EG getCtx
(?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)))))
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G
jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
@TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
context:
G T Tm : Type
EG : G → G → Type
ET : T → T → Type
ETm : Tm → Tm → Type
EGrfl : {Γ : G} → EG Γ Γ
getCtx : T → G
getTy : Tm → T
GAlgebra : CtxSyntaxLayer G T EG getCtx → G
TAlgebra : TySyntaxLayer G T EG getCtx → T
Γ✝ : G
⊢ G

71
tests/lean/run/state8.lean Normal file
View file

@ -0,0 +1,71 @@
inductive States | s0 | s1 | s2 | s3 | s4 | s5 | s6 | s7
open States
def f : States → States → States
| s0, s0 => s0
| s0, s1 => s0
| s0, s2 => s0
| s0, s3 => s0
| s0, s4 => s0
| s0, s5 => s0
| s0, s6 => s0
| s0, s7 => s0
| s1, s0 => s0
| s1, s1 => s0
| s1, s2 => s0
| s1, s3 => s0
| s1, s4 => s0
| s1, s5 => s0
| s1, s6 => s0
| s1, s7 => s0
| s2, s0 => s0
| s2, s1 => s0
| s2, s2 => s0
| s2, s3 => s0
| s2, s4 => s0
| s2, s5 => s0
| s2, s6 => s0
| s2, s7 => s0
| s3, s0 => s0
| s3, s1 => s0
| s3, s2 => s0
| s3, s3 => s0
| s3, s4 => s0
| s3, s5 => s0
| s3, s6 => s0
| s3, s7 => s0
| s4, s0 => s0
| s4, s1 => s0
| s4, s2 => s0
| s4, s3 => s0
| s4, s4 => s0
| s4, s5 => s0
| s4, s6 => s0
| s4, s7 => s0
| s5, s0 => s0
| s5, s1 => s0
| s5, s2 => s0
| s5, s3 => s0
| s5, s4 => s0
| s5, s5 => s0
| s5, s6 => s0
| s5, s7 => s0
| s6, s0 => s0
| s6, s1 => s0
| s6, s2 => s0
| s6, s3 => s0
| s6, s4 => s0
| s6, s5 => s0
| s6, s6 => s0
| s6, s7 => s0
| s7, s0 => s0
| s7, s1 => s0
| s7, s2 => s0
| s7, s3 => s0
| s7, s4 => s0
| s7, s5 => s0
| s7, s6 => s0
| s7, s7 => s0
set_option maxHeartbeats 0
example : ∀ x y z, f (f (f s0 x) y) z = f (f x z) (f y z) := by
intros x y z
cases x <;> cases y <;> cases z <;> rfl