chore: fix tests
This commit is contained in:
Leonardo de Moura
parent
4b58c4cc02
commit
4239ae69f6
5 changed files with 49 additions and 63 deletions
|
|
@ -16,7 +16,7 @@ abbrev Catish : CatIsh :=
|
|||
|
||||
universe m o
|
||||
unif_hint (mvar : CatIsh) where
|
||||
Catish.{o,m} =?= mvar |- mvar.Obj =?= CatIsh.{m,o}
|
||||
Catish.{m, o} =?= mvar |- mvar.Obj =?= CatIsh.{m,o}
|
||||
|
||||
structure CtxSyntaxLayerParamsObj where
|
||||
Ct : CatIsh
|
||||
|
|
|
|||
|
|
@ -1,11 +1,9 @@
|
|||
423.lean:3:35-3:40: error: application type mismatch
|
||||
HAdd.hAdd (α := Nat) a
|
||||
argument
|
||||
a
|
||||
423.lean:3:39-3:40: error: type mismatch
|
||||
0
|
||||
has type
|
||||
T : Sort u
|
||||
but is expected to have type
|
||||
Nat : Type
|
||||
but is expected to have type
|
||||
T : Sort u
|
||||
423.lean:5:33-5:38: error: application type mismatch
|
||||
Add T
|
||||
argument
|
||||
|
|
@ -22,11 +20,9 @@ has type
|
|||
Sort u : Type u
|
||||
but is expected to have type
|
||||
Type ?u : Type (?u + 1)
|
||||
423.lean:5:55-5:60: error: application type mismatch
|
||||
HAdd.hAdd (α := Nat) a
|
||||
argument
|
||||
a
|
||||
423.lean:5:59-5:60: error: type mismatch
|
||||
0
|
||||
has type
|
||||
T : Sort u
|
||||
but is expected to have type
|
||||
Nat : Type
|
||||
but is expected to have type
|
||||
T : Sort u
|
||||
|
|
|
|||
|
|
@ -1,9 +1,9 @@
|
|||
[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.535} @ ⟨13, 11⟩-⟨13, 14⟩
|
||||
[.] `Nat : some Sort.{?_uniq.405} @ ⟨13, 11⟩-⟨13, 14⟩
|
||||
Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
|
||||
x : Nat @ ⟨13, 7⟩-⟨13, 8⟩
|
||||
Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ myMacro._@.Init.Notation._hyg.2258
|
||||
Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ myMacro._@.Init.Notation._hyg.2315
|
||||
Macro expansion
|
||||
Nat × Nat
|
||||
===>
|
||||
|
|
@ -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.539} @ ⟨13, 18⟩-⟨13, 21⟩
|
||||
[.] `Nat : some Type.{?_uniq.409} @ ⟨13, 18⟩-⟨13, 21⟩
|
||||
Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
|
||||
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Type.{?_uniq.538} @ ⟨13, 24⟩-⟨13, 27⟩
|
||||
[.] `Nat : some Type.{?_uniq.408} @ ⟨13, 24⟩-⟨13, 27⟩
|
||||
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
|
||||
let y := (x, x);
|
||||
id y : Nat × Nat @ ⟨14, 2⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabLetDecl
|
||||
|
|
@ -39,39 +39,33 @@
|
|||
[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.566} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
[.] `Nat : some Sort.{?_uniq.436} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
x : Nat @ ⟨17, 9⟩-⟨17, 10⟩
|
||||
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.568} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
[.] `Nat : some Sort.{?_uniq.438} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
y : 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.571} @ ⟨17, 27⟩-⟨17, 31⟩
|
||||
[.] `Bool : some Sort.{?_uniq.441} @ ⟨17, 27⟩-⟨17, 31⟩
|
||||
Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
|
||||
b : Bool @ ⟨17, 23⟩-⟨17, 24⟩
|
||||
x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ myMacro._@.Init.Notation._hyg.9563
|
||||
x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ myMacro._@.Init.Notation._hyg.9571
|
||||
Macro expansion
|
||||
x + 0 = x
|
||||
===>
|
||||
binrel% Eq✝ (x + 0)x
|
||||
x + 0 = x : Prop @ ⟨17, 35⟩†-⟨17, 44⟩ @ Lean.Elab.Term.elabBinRel
|
||||
x + 0 : Nat @ ⟨17, 35⟩-⟨17, 40⟩ @ myMacro._@.Init.Notation._hyg.5829
|
||||
x + 0 : Nat @ ⟨17, 35⟩-⟨17, 40⟩ @ myMacro._@.Init.Notation._hyg.6125
|
||||
Macro expansion
|
||||
x + 0
|
||||
===>
|
||||
binop% HAdd.hAdd✝ x 0
|
||||
x + 0 : Nat @ ⟨17, 35⟩†-⟨17, 40⟩ @ Lean.Elab.Term.elabBinOp
|
||||
Macro expansion
|
||||
binop% HAdd.hAdd✝ x 0
|
||||
===>
|
||||
HAdd.hAdd✝ x 0
|
||||
x + 0 : Nat @ ⟨17, 35⟩†-⟨17, 40⟩ @ Lean.Elab.Term.elabApp
|
||||
HAdd.hAdd : {α β γ : Type} → [self : HAdd α β γ] → α → β → γ @ ⟨17, 35⟩†-⟨17, 40⟩†
|
||||
x : Nat @ ⟨17, 35⟩-⟨17, 36⟩ @ Lean.Elab.Term.elabIdent
|
||||
x : Nat @ ⟨17, 35⟩-⟨17, 36⟩
|
||||
0 : Nat @ ⟨17, 39⟩-⟨17, 40⟩ @ Lean.Elab.Term.elabNumLit
|
||||
x + 0 : Nat @ ⟨17, 35⟩†-⟨17, 40⟩ @ Lean.Elab.Term.BinOp.elabBinOp'
|
||||
x : Nat @ ⟨17, 35⟩-⟨17, 36⟩ @ Lean.Elab.Term.elabIdent
|
||||
x : Nat @ ⟨17, 35⟩-⟨17, 36⟩
|
||||
0 : Nat @ ⟨17, 39⟩-⟨17, 40⟩ @ Lean.Elab.Term.elabNumLit
|
||||
x : Nat @ ⟨17, 43⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabIdent
|
||||
x : Nat @ ⟨17, 43⟩-⟨17, 44⟩
|
||||
fun x y b =>
|
||||
|
|
@ -115,20 +109,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.818} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
[.] `Nat : some Sort.{?_uniq.591} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
x : Nat @ ⟨21, 10⟩-⟨21, 11⟩
|
||||
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.820} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
[.] `Nat : some Sort.{?_uniq.593} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
y : 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.823} @ ⟨21, 28⟩-⟨21, 32⟩
|
||||
[.] `Bool : some Sort.{?_uniq.596} @ ⟨21, 28⟩-⟨21, 32⟩
|
||||
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
|
||||
b : Bool @ ⟨21, 24⟩-⟨21, 25⟩
|
||||
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.825} @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
[.] `Nat : some Sort.{?_uniq.598} @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
fun x y b =>
|
||||
let x := (x + y, x - y);
|
||||
|
|
@ -170,22 +164,22 @@
|
|||
Prod.mk✝ (x + y) (x - y)
|
||||
(x + y, x - y) : Nat × Nat @ ⟨23, 18⟩†-⟨23, 31⟩ @ Lean.Elab.Term.elabApp
|
||||
Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 18⟩†-⟨23, 32⟩†
|
||||
x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ myMacro._@.Init.Notation._hyg.5829
|
||||
x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩ @ myMacro._@.Init.Notation._hyg.6125
|
||||
Macro expansion
|
||||
x + y
|
||||
===>
|
||||
binop% HAdd.hAdd✝ x y
|
||||
x + y : Nat @ ⟨23, 19⟩†-⟨23, 24⟩ @ Lean.Elab.Term.elabBinOp
|
||||
x + y : Nat @ ⟨23, 19⟩†-⟨23, 24⟩ @ Lean.Elab.Term.BinOp.elabBinOp'
|
||||
x : Nat @ ⟨23, 19⟩-⟨23, 20⟩ @ Lean.Elab.Term.elabIdent
|
||||
x : Nat @ ⟨23, 19⟩-⟨23, 20⟩
|
||||
y : Nat @ ⟨23, 23⟩-⟨23, 24⟩ @ Lean.Elab.Term.elabIdent
|
||||
y : Nat @ ⟨23, 23⟩-⟨23, 24⟩
|
||||
x - y : Nat @ ⟨23, 26⟩-⟨23, 31⟩ @ myMacro._@.Init.Notation._hyg.5925
|
||||
x - y : Nat @ ⟨23, 26⟩-⟨23, 31⟩ @ myMacro._@.Init.Notation._hyg.6221
|
||||
Macro expansion
|
||||
x - y
|
||||
===>
|
||||
binop% HSub.hSub✝ x y
|
||||
x - y : Nat @ ⟨23, 26⟩†-⟨23, 31⟩ @ Lean.Elab.Term.elabBinOp
|
||||
x - y : Nat @ ⟨23, 26⟩†-⟨23, 31⟩ @ Lean.Elab.Term.BinOp.elabBinOp'
|
||||
x : Nat @ ⟨23, 26⟩-⟨23, 27⟩ @ Lean.Elab.Term.elabIdent
|
||||
x : Nat @ ⟨23, 26⟩-⟨23, 27⟩
|
||||
y : Nat @ ⟨23, 30⟩-⟨23, 31⟩ @ Lean.Elab.Term.elabIdent
|
||||
|
|
@ -209,29 +203,29 @@
|
|||
let z1 := z + w;
|
||||
z + z1 : Nat @ ⟨24, 4⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabLetDecl
|
||||
Nat : Type @ ⟨24, 8⟩†-⟨24, 10⟩† @ Lean.Elab.Term.elabHole
|
||||
z + w : Nat @ ⟨24, 14⟩-⟨24, 19⟩ @ myMacro._@.Init.Notation._hyg.5829
|
||||
z + w : Nat @ ⟨24, 14⟩-⟨24, 19⟩ @ myMacro._@.Init.Notation._hyg.6125
|
||||
Macro expansion
|
||||
z + w
|
||||
===>
|
||||
binop% HAdd.hAdd✝ z w
|
||||
z + w : Nat @ ⟨24, 14⟩†-⟨24, 19⟩ @ Lean.Elab.Term.elabBinOp
|
||||
z + w : Nat @ ⟨24, 14⟩†-⟨24, 19⟩ @ Lean.Elab.Term.BinOp.elabBinOp'
|
||||
z : Nat @ ⟨24, 14⟩-⟨24, 15⟩ @ Lean.Elab.Term.elabIdent
|
||||
z : Nat @ ⟨24, 14⟩-⟨24, 15⟩
|
||||
w : Nat @ ⟨24, 18⟩-⟨24, 19⟩ @ Lean.Elab.Term.elabIdent
|
||||
w : Nat @ ⟨24, 18⟩-⟨24, 19⟩
|
||||
z1 : Nat @ ⟨24, 8⟩-⟨24, 10⟩
|
||||
z + z1 : Nat @ ⟨25, 4⟩-⟨25, 10⟩ @ myMacro._@.Init.Notation._hyg.5829
|
||||
z + z1 : Nat @ ⟨25, 4⟩-⟨25, 10⟩ @ myMacro._@.Init.Notation._hyg.6125
|
||||
Macro expansion
|
||||
z + z1
|
||||
===>
|
||||
binop% HAdd.hAdd✝ z z1
|
||||
z + z1 : Nat @ ⟨25, 4⟩†-⟨25, 10⟩ @ Lean.Elab.Term.elabBinOp
|
||||
z + z1 : Nat @ ⟨25, 4⟩†-⟨25, 10⟩ @ Lean.Elab.Term.BinOp.elabBinOp'
|
||||
z : Nat @ ⟨25, 4⟩-⟨25, 5⟩ @ Lean.Elab.Term.elabIdent
|
||||
z : Nat @ ⟨25, 4⟩-⟨25, 5⟩
|
||||
z1 : Nat @ ⟨25, 8⟩-⟨25, 10⟩ @ Lean.Elab.Term.elabIdent
|
||||
z1 : Nat @ ⟨25, 8⟩-⟨25, 10⟩
|
||||
[Elab.info] command @ ⟨27, 0⟩-⟨28, 17⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
Nat × Array (Array Nat) : Type @ ⟨27, 12⟩-⟨27, 35⟩ @ myMacro._@.Init.Notation._hyg.2258
|
||||
Nat × Array (Array Nat) : Type @ ⟨27, 12⟩-⟨27, 35⟩ @ myMacro._@.Init.Notation._hyg.2315
|
||||
Macro expansion
|
||||
Nat × Array (Array Nat)
|
||||
===>
|
||||
|
|
@ -239,10 +233,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.1520} @ ⟨27, 12⟩-⟨27, 15⟩
|
||||
[.] `Nat : some Type.{?_uniq.800} @ ⟨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.1519} @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
[.] `Array : some Type.{?_uniq.799} @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen
|
||||
Macro expansion
|
||||
|
|
@ -250,17 +244,17 @@
|
|||
===>
|
||||
Array Nat
|
||||
Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Array : some Type.{?_uniq.1521} @ ⟨27, 25⟩-⟨27, 30⟩
|
||||
[.] `Array : some Type.{?_uniq.801} @ ⟨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.1522} @ ⟨27, 31⟩-⟨27, 34⟩
|
||||
[.] `Nat : some Type.{?_uniq.802} @ ⟨27, 31⟩-⟨27, 34⟩
|
||||
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
|
||||
s : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
|
||||
Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Array : some Sort.{?_uniq.1524} @ ⟨27, 39⟩-⟨27, 44⟩
|
||||
[.] `Array : some Sort.{?_uniq.804} @ ⟨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.1525} @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
[.] `Nat : some Type.{?_uniq.805} @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp
|
||||
s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩
|
||||
|
|
@ -274,11 +268,11 @@
|
|||
Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩
|
||||
[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.1568} @ ⟨30, 14⟩-⟨30, 15⟩
|
||||
[.] `B : some Sort.{?_uniq.848} @ ⟨30, 14⟩-⟨30, 15⟩
|
||||
B : Type @ ⟨30, 14⟩-⟨30, 15⟩
|
||||
arg : B @ ⟨30, 8⟩-⟨30, 11⟩
|
||||
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.1570} @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
[.] `Nat : some Sort.{?_uniq.850} @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp
|
||||
arg : B @ ⟨31, 2⟩-⟨31, 5⟩
|
||||
|
|
@ -291,11 +285,11 @@
|
|||
0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabNumLit
|
||||
[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.1592} @ ⟨33, 12⟩-⟨33, 15⟩
|
||||
[.] `Nat : some Sort.{?_uniq.872} @ ⟨33, 12⟩-⟨33, 15⟩
|
||||
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
|
||||
x : Nat @ ⟨33, 8⟩-⟨33, 9⟩
|
||||
B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `B : some Sort.{?_uniq.1594} @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
[.] `B : some Sort.{?_uniq.874} @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
B : Type @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
{ pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst
|
||||
({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩ @ Lean.Elab.Term.expandParen
|
||||
|
|
|
|||
|
|
@ -12,8 +12,6 @@ macroStack.lean:11:9-11:15: error: invalid use of `(<- ...)`, must be nested ins
|
|||
macroStack.lean:17:0-17:6: error: failed to synthesize instance
|
||||
HAdd Nat String ?m
|
||||
with resulting expansion
|
||||
HAdd.hAdd✝ (x + x✝) x✝¹
|
||||
while expanding
|
||||
binop% HAdd.hAdd✝ (x + x✝)x✝¹
|
||||
while expanding
|
||||
(x + x✝) + x✝¹
|
||||
|
|
|
|||
|
|
@ -1,9 +1,7 @@
|
|||
typeOf.lean:11:21-11:24: error: type mismatch
|
||||
x + 1
|
||||
has type
|
||||
Nat : Type
|
||||
but is expected to have type
|
||||
Bool : Type
|
||||
typeOf.lean:11:21-11:24: error: failed to synthesize instance
|
||||
HAdd Nat Nat Bool
|
||||
typeOf.lean:12:0-12:5: error: failed to synthesize instance
|
||||
HAdd Bool Nat Nat
|
||||
typeOf.lean:20:54-20:60: error: invalid reassignment, term has type
|
||||
Bool : Type
|
||||
but is expected to have type
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue