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

fix: tolerate type incorrect terms

Browse source 
This bug was producing a type error when I was using `set_option trace.Elab true`
This commit is contained in:
Leonardo de Moura 2021-04-29 21:29:05 -07:00
parent d54c964a51
commit adae6fdb40
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Elab/InfoTree.lean
View file

@ -156,7 +156,10 @@ def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : IO
def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
info.runMetaM ctx do
return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {formatStxRange ctx info.stx}"
try
return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {formatStxRange ctx info.stx}"
catch _ =>
return f!"{← Meta.ppExpr info.expr} : <failed-to-infer-type> @ {formatStxRange ctx info.stx}"
def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
match info with

4
tests/lean/run/traceElabIssue.lean Normal file
View file

@ -0,0 +1,4 @@
set_option trace.Elab true
inductive Vec (α : Type u) : Nat → Type u
| nil : Vec α Nat.zero
| cons {n : Nat} : (head : α) → (tail : Vec α n) → Vec α (Nat.succ n)