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

chore: improve Array Expr to MessageData coercion

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-21 10:40:39 -08:00
parent 64907481d7
commit f7d63c0453
1 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/Init/Lean/Message.lean
View file

@ -65,7 +65,17 @@ instance coeOfFormat : HasCoe Format MessageData := ⟨ofFormat⟩
instance coeOfLevel : HasCoe Level MessageData := ⟨ofLevel⟩
instance coeOfExpr : HasCoe Expr MessageData := ⟨ofExpr⟩
instance coeOfName : HasCoe Name MessageData := ⟨ofName⟩
instance coeOfArrayExpr : HasCoe (Array Expr) MessageData := ⟨fun es => node $ es.map $ fun e => ofExpr e⟩
partial def arrayExpr.toMessageData (es : Array Expr) : Nat → MessageData → MessageData
| i, acc =>
if h : i < es.size then
let e := es.get ⟨i, h⟩;
let acc := if i == 0 then acc ++ ofExpr e else acc ++ ", " ++ ofExpr e;
arrayExpr.toMessageData (i+1) acc
else
acc ++ "]"
instance coeOfArrayExpr : HasCoe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩
end MessageData