Skip to content

Commit

Permalink
fix test
Browse files Browse the repository at this point in the history
  • Loading branch information
kmill committed Oct 7, 2024
1 parent a5c8b3f commit b19cf9f
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions tests/lean/1018unknowMVarIssue.lean.expected.out
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,8 @@ a : α
• Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
• α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
• a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
• FVarAlias a: _uniq.636 -> _uniq.312
• FVarAlias α: _uniq.635 -> _uniq.310
• FVarAlias a: _uniq.675 -> _uniq.312
• FVarAlias α: _uniq.674 -> _uniq.310
• ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
• [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
• Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
Expand All @@ -70,8 +70,8 @@ a : α
• Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
• n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
• a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
• FVarAlias a: _uniq.667 -> _uniq.312
• FVarAlias n: _uniq.666 -> _uniq.310
• FVarAlias a: _uniq.706 -> _uniq.312
• FVarAlias n: _uniq.705 -> _uniq.310
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
• [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
Expand Down

0 comments on commit b19cf9f

Please sign in to comment.