sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

test: update expected output for instance priority change

Browse Source 
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Kim Morrison
2026-03-04 12:39:20 +00:00
parent 209af53427
commit 9e94b2e35b
3 changed files with 6 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
tests/elab/info_trees.lean
View File

@@ -62,7 +62,7 @@ info: • [Command] @ ⟨79, 0⟩-⟨79, 40⟩ @ Lean.Elab.Command.elabDeclarati
⊢ 0 ≤ n
after no goals
• [Term] Nat.zero_le n : 0 ≤ n @ ⟨1, 1⟩†-⟨1, 1⟩† @ Lean.Elab.Term.elabApp
• [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.35.3 @ ⟨1, 0⟩†-⟨1, 0⟩†
• [Completion-Id] Nat.zero_le : some LE.le.{0} Nat instLENat (OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)) _uniq.47.3 @ ⟨1, 0⟩†-⟨1, 0⟩†
• [Term] Nat.zero_le : ∀ (n : Nat), 0 ≤ n @ ⟨1, 0⟩†-⟨1, 0⟩†
• [Term] n : Nat @ ⟨1, 5⟩†-⟨1, 5⟩† @ Lean.Elab.Term.elabIdent
• [Completion-Id] n : some Nat @ ⟨1, 5⟩†-⟨1, 5⟩†

6
tests/elab/setOptionTermTactic.lean.out.expected
View File

@@ -1,8 +1,8 @@
[Meta.synthInstance] 💥️ OfNat ?m 1
[Meta.synthInstance] new goal OfNat ?m 1
[Meta.synthInstance.instances] #[@Lean.Grind.Semiring.ofNat, @One.toOfNat1, @Int16.instOfNat, @UInt64.instOfNat, @Rat.instOfNat, @Int8.instOfNat, @instOfNatFloat, @BitVec.instOfNat, Dyadic.instOfNat, @Int64.instOfNat, @instOfNat, @Id.instOfNat, @UInt16.instOfNat, instOfNatNat, @UInt32.instOfNat, @UInt8.instOfNat, @Fin.instOfNat, @ISize.instOfNat, @instOfNatFloat32, @Int32.instOfNat, @USize.instOfNat]
[Meta.synthInstance.apply] 💥️ apply @USize.instOfNat to OfNat ?m 1
[Meta.synthInstance.tryResolve] 💥️ OfNat ?m 1 ≟ OfNat USize ?m
[Meta.synthInstance.instances] #[@Lean.Grind.Semiring.ofNat, @One.toOfNat1, @Int16.instOfNat, @UInt64.instOfNat, @Rat.instOfNat, @Int8.instOfNat, @instOfNatFloat, @BitVec.instOfNat, Dyadic.instOfNat, @Int64.instOfNat, @instOfNat, @Id.instOfNat, @UInt16.instOfNat, instOfNatNat, @UInt32.instOfNat, @UInt8.instOfNat, @Fin.instOfNat, @ISize.instOfNat, @instOfNatFloat32, @Int32.instOfNat, @USize.instOfNat, @Lean.Grind.CommRing.OfCommSemiring.instOfNatQ]
[Meta.synthInstance.apply] 💥️ apply @Lean.Grind.CommRing.OfCommSemiring.instOfNatQ to OfNat ?m 1
[Meta.synthInstance.tryResolve] 💥️ OfNat ?m 1 ≟ OfNat (Lean.Grind.Ring.OfSemiring.Q ?m) ?m
[Meta.Tactic.simp.rewrite] Nat.add_succ:1000:
x + 1
==>

4
tests/lean/interactive/completionPrefixIssue.lean.expected.out
View File

@@ -3,7 +3,7 @@
{"items":
[{"label": "veryLongDefinitionName",
"kind": 6,
"data": ["file:///completionPrefixIssue.lean", 1, 64, 0, "f_uniq.39"]},
"data": ["file:///completionPrefixIssue.lean", 1, 64, 0, "f_uniq.51"]},
{"label": "veryLongDefinitionNameVeryLongDefinitionName",
"kind": 21,
"data":
@@ -17,7 +17,7 @@ Resolution of veryLongDefinitionName:
{"label": "veryLongDefinitionName",
"kind": 6,
"detail": "Nat",
"data": ["file:///completionPrefixIssue.lean", 1, 64, 0, "f_uniq.39"]}
"data": ["file:///completionPrefixIssue.lean", 1, 64, 0, "f_uniq.51"]}
Resolution of veryLongDefinitionNameVeryLongDefinitionName:
{"label": "veryLongDefinitionNameVeryLongDefinitionName",
"kind": 21,