chore: fix tests
This commit is contained in:
Leonardo de Moura
parent
8fbe7062fa
commit
15e6dd262d
4 changed files with 79 additions and 79 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -41,16 +41,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.448} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
[.] `Nat : some Sort.{?_uniq.450} @ ⟨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.450} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
[.] `Nat : some Sort.{?_uniq.452} @ ⟨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.453} @ ⟨17, 27⟩-⟨17, 31⟩
|
||||
[.] `Bool : some Sort.{?_uniq.455} @ ⟨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»
|
||||
|
|
@ -112,20 +112,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.567} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
[.] `Nat : some Sort.{?_uniq.574} @ ⟨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.569} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
[.] `Nat : some Sort.{?_uniq.576} @ ⟨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.572} @ ⟨21, 28⟩-⟨21, 32⟩
|
||||
[.] `Bool : some Sort.{?_uniq.579} @ ⟨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.574} @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
[.] `Nat : some Sort.{?_uniq.581} @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
fun x y b =>
|
||||
let x := (x + y, x - y);
|
||||
|
|
@ -238,10 +238,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.772} @ ⟨27, 12⟩-⟨27, 15⟩
|
||||
[.] `Nat : some Type.{?_uniq.787} @ ⟨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.771} @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
[.] `Array : some Type.{?_uniq.786} @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen
|
||||
Macro expansion
|
||||
|
|
@ -249,17 +249,17 @@
|
|||
===>
|
||||
Array Nat
|
||||
Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Array : some Type.{?_uniq.773} @ ⟨27, 25⟩-⟨27, 30⟩
|
||||
[.] `Array : some Type.{?_uniq.788} @ ⟨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.774} @ ⟨27, 31⟩-⟨27, 34⟩
|
||||
[.] `Nat : some Type.{?_uniq.789} @ ⟨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.776} @ ⟨27, 39⟩-⟨27, 44⟩
|
||||
[.] `Array : some Sort.{?_uniq.791} @ ⟨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.777} @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
[.] `Nat : some Type.{?_uniq.792} @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
s (isBinder := true) : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
|
||||
Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp
|
||||
|
|
@ -275,11 +275,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.818} @ ⟨30, 14⟩-⟨30, 15⟩
|
||||
[.] `B : some Sort.{?_uniq.834} @ ⟨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.820} @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
[.] `Nat : some Sort.{?_uniq.836} @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
arg (isBinder := true) : B @ ⟨30, 8⟩-⟨30, 11⟩
|
||||
A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp
|
||||
|
|
@ -294,11 +294,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.840} @ ⟨33, 12⟩-⟨33, 15⟩
|
||||
[.] `Nat : some Sort.{?_uniq.857} @ ⟨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.842} @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
[.] `B : some Sort.{?_uniq.859} @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
B : Type @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
x (isBinder := true) : Nat @ ⟨33, 8⟩-⟨33, 9⟩
|
||||
{ pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst
|
||||
|
|
@ -338,73 +338,73 @@ 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.863} @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
[.] `Nat : some Sort.{?_uniq.881} @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
_uniq.864 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
|
||||
_uniq.882 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
|
||||
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.865} @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
[.] `Nat : some Sort.{?_uniq.883} @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
Nat : Type @ ⟨45, 14⟩-⟨45, 17⟩
|
||||
_uniq.866 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
|
||||
Eq.{1} Nat _uniq.864 _uniq.864 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
|
||||
_uniq.884 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
|
||||
Eq.{1} Nat _uniq.882 _uniq.882 : Prop @ ⟨45, 21⟩-⟨45, 26⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
|
||||
Macro expansion
|
||||
(«term_=_» `x "=" `x)
|
||||
===>
|
||||
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.177 `x `x)
|
||||
Eq.{1} Nat _uniq.864 _uniq.864 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel
|
||||
_uniq.864 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.864 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
|
||||
_uniq.864 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.864 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
|
||||
_uniq.873 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
|
||||
_uniq.874 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
|
||||
(fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.873 _uniq.874]) f6.f7 : Eq.{1} Nat _uniq.873 _uniq.873 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
|
||||
Eq.{1} Nat _uniq.882 _uniq.882 : Prop @ ⟨45, 21⟩†-⟨45, 26⟩ @ Lean.Elab.Term.elabBinRel
|
||||
_uniq.882 : Nat @ ⟨45, 21⟩-⟨45, 22⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.882 : Nat @ ⟨45, 21⟩-⟨45, 22⟩
|
||||
_uniq.882 : Nat @ ⟨45, 25⟩-⟨45, 26⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.882 : Nat @ ⟨45, 25⟩-⟨45, 26⟩
|
||||
_uniq.891 (isBinder := true) : Nat @ ⟨45, 8⟩-⟨45, 9⟩
|
||||
_uniq.892 (isBinder := true) : Nat @ ⟨45, 10⟩-⟨45, 11⟩
|
||||
(fun (f7 : forall (x : Nat), Nat -> (Eq.{1} Nat x x)) => [mdata _recApp: f7 _uniq.891 _uniq.892]) f6.f7 : Eq.{1} Nat _uniq.891 _uniq.891 @ ⟨46, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabLetRec
|
||||
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.875} @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
[.] `Nat : some Sort.{?_uniq.893} @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
_uniq.876 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
|
||||
_uniq.894 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
|
||||
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.877} @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
[.] `Nat : some Sort.{?_uniq.895} @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
Nat : Type @ ⟨46, 20⟩-⟨46, 23⟩
|
||||
_uniq.878 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
|
||||
Eq.{1} Nat _uniq.876 _uniq.876 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
|
||||
_uniq.896 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
|
||||
Eq.{1} Nat _uniq.894 _uniq.894 : Prop @ ⟨46, 27⟩-⟨46, 32⟩ @ «_aux_Init_Notation___macroRules_term_=__2»
|
||||
Macro expansion
|
||||
(«term_=_» `x "=" `x)
|
||||
===>
|
||||
(Term.binrel "binrel%" `Eq._@.infoTree._hyg.185 `x `x)
|
||||
Eq.{1} Nat _uniq.876 _uniq.876 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel
|
||||
_uniq.876 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.876 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
|
||||
_uniq.876 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.876 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
|
||||
_uniq.883 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
|
||||
_uniq.886 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
|
||||
_uniq.887 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
|
||||
Eq.refl.{1} Nat _uniq.886 : Eq.{1} Nat _uniq.886 _uniq.886 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Eq.refl : some Eq.{?_uniq.880} Nat _uniq.886 _uniq.886 @ ⟨46, 36⟩-⟨46, 43⟩
|
||||
Eq.{1} Nat _uniq.894 _uniq.894 : Prop @ ⟨46, 27⟩†-⟨46, 32⟩ @ Lean.Elab.Term.elabBinRel
|
||||
_uniq.894 : Nat @ ⟨46, 27⟩-⟨46, 28⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.894 : Nat @ ⟨46, 27⟩-⟨46, 28⟩
|
||||
_uniq.894 : Nat @ ⟨46, 31⟩-⟨46, 32⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.894 : Nat @ ⟨46, 31⟩-⟨46, 32⟩
|
||||
_uniq.901 (isBinder := true) : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨46, 10⟩-⟨46, 12⟩
|
||||
_uniq.904 (isBinder := true) : Nat @ ⟨46, 14⟩-⟨46, 15⟩
|
||||
_uniq.905 (isBinder := true) : Nat @ ⟨46, 16⟩-⟨46, 17⟩
|
||||
Eq.refl.{1} Nat _uniq.904 : Eq.{1} Nat _uniq.904 _uniq.904 @ ⟨46, 36⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Eq.refl : some Eq.{?_uniq.898} Nat _uniq.904 _uniq.904 @ ⟨46, 36⟩-⟨46, 43⟩
|
||||
Eq.refl.{1} : forall {α : Type} (a : α), Eq.{1} α a a @ ⟨46, 36⟩-⟨46, 43⟩
|
||||
_uniq.886 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.886 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
|
||||
[mdata _recApp: _uniq.883 _uniq.873 _uniq.874] : Eq.{1} Nat _uniq.873 _uniq.873 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
|
||||
_uniq.883 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
|
||||
_uniq.873 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.873 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
|
||||
_uniq.874 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.874 : Nat @ ⟨47, 7⟩-⟨47, 8⟩
|
||||
_uniq.904 : Nat @ ⟨46, 44⟩-⟨46, 45⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.904 : Nat @ ⟨46, 44⟩-⟨46, 45⟩
|
||||
[mdata _recApp: _uniq.901 _uniq.891 _uniq.892] : Eq.{1} Nat _uniq.891 _uniq.891 @ ⟨47, 2⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabApp
|
||||
_uniq.901 : forall (x : Nat), Nat -> (Eq.{1} Nat x x) @ ⟨47, 2⟩-⟨47, 4⟩
|
||||
_uniq.891 : Nat @ ⟨47, 5⟩-⟨47, 6⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.891 : Nat @ ⟨47, 5⟩-⟨47, 6⟩
|
||||
_uniq.892 : Nat @ ⟨47, 7⟩-⟨47, 8⟩ @ Lean.Elab.Term.elabIdent
|
||||
_uniq.892 : 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.910} @ ⟨50, 12⟩-⟨50, 13⟩
|
||||
[.] `B : some Sort.{?_uniq.929} @ ⟨50, 12⟩-⟨50, 13⟩
|
||||
B : Type @ ⟨50, 12⟩-⟨50, 13⟩
|
||||
_uniq.911 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
|
||||
_uniq.930 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
|
||||
B : Type @ ⟨50, 17⟩-⟨50, 18⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `B : some Sort.{?_uniq.912} @ ⟨50, 17⟩-⟨50, 18⟩
|
||||
[.] `B : some Sort.{?_uniq.931} @ ⟨50, 17⟩-⟨50, 18⟩
|
||||
B : Type @ ⟨50, 17⟩-⟨50, 18⟩
|
||||
_uniq.915 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
|
||||
B.mk (B.pair _uniq.915) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
|
||||
B.pair _uniq.915 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
|
||||
_uniq.915 : B @ ⟨50, 24⟩-⟨50, 25⟩
|
||||
[.] _uniq.915 : B @ ⟨50, 24⟩-⟨50, 25⟩ : some Prod.{0 0} A A
|
||||
_uniq.934 (isBinder := true) : B @ ⟨50, 8⟩-⟨50, 9⟩
|
||||
B.mk (B.pair _uniq.934) : B @ ⟨50, 22⟩-⟨50, 32⟩ @ Lean.Elab.Term.StructInst.elabStructInst
|
||||
B.pair _uniq.934 : Prod.{0 0} A A @ ⟨50, 24⟩-⟨50, 25⟩† @ Lean.Elab.Term.elabProj
|
||||
_uniq.934 : B @ ⟨50, 24⟩-⟨50, 25⟩
|
||||
[.] _uniq.934 : 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.915 @ ⟨50, 22⟩†-⟨50, 32⟩
|
||||
pair : Prod.{0 0} A A := B.pair _uniq.934 @ ⟨50, 22⟩†-⟨50, 32⟩
|
||||
f7 (isBinder := true) : B -> B @ ⟨50, 4⟩-⟨50, 6⟩
|
||||
|
|
|
|||
|
|
@ -101,21 +101,6 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
|
|||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : 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 x✝¹ x✝)
|
||||
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
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : 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 x✝¹ x✝)
|
||||
context:
|
||||
|
|
@ -131,3 +116,18 @@ TAlgebra : TySyntaxLayer G T EG getCtx → T
|
|||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : 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 x✝¹ x✝)
|
||||
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
|
||||
x✝¹ : TmSyntaxLayer G T Tm EG ET getCtx getTy TAlgebra
|
||||
x✝ : G
|
||||
⊢ G
|
||||
|
|
|
|||
|
|
@ -11,4 +11,4 @@ argument #2 was not used for structural recursion
|
|||
|
||||
structural recursion cannot be used
|
||||
|
||||
'termination_by' modifier missing
|
||||
well-founded recursion cannot be used, function 'g' contains application of function 'g' with #1 argument(s), but function has arity 2
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue