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

feat: change Meta.Exception.other constructor

Browse source
This commit is contained in:
Leonardo de Moura 2020-07-30 13:06:57 -07:00
parent 98e9fc20d5
commit e22e900784
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Meta/Exception.lean
View file

@ -39,7 +39,7 @@ inductive Exception
| generalizeTelescope (es : Array Expr) (ctx : ExceptionContext)
| kernel (ex : KernelException) (opts : Options)
| bug (b : Bug) (ctx : ExceptionContext)
| other (msg : String)
| other (msg : MessageData)
namespace Exception
instance : Inhabited Exception := ⟨other ""⟩
@ -68,7 +68,7 @@ def toStr : Exception → String
| generalizeTelescope _ _ => "generalize telescope"
| kernel _ _ => "kernel exception"
| bug _ _ => "bug"
| other s => s
| other s => toString $ fmt s
instance : HasToString Exception := ⟨toStr⟩