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

chore: minor adjustments

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-22 14:57:26 -07:00
parent 13faf9fdf6
commit 16099189f2
2 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -49,17 +49,17 @@ partial def formatAux : Option (Environment × MetavarContext × LocalContext)
| none, ofExpr e => "<expr>"
| some (env, mctx, lctx), ofExpr e => "<expr>" -- TODO: invoke pretty printer
| _, context env mctx lctx d => formatAux (some (env, mctx, lctx)) d
| ctx, tagged cls d => Format.sbracket (format cls) ++ " " ++ Format.nest 2 (formatAux ctx d)
| ctx, tagged cls d => Format.sbracket (format cls) ++ " " ++ formatAux ctx d
| ctx, nest n d => Format.nest n (formatAux ctx d)
| ctx, compose d₁ d₂ => formatAux ctx d₁ ++ formatAux ctx d₂
| ctx, group d => Format.group (formatAux ctx d)
| ctx, node ds => ds.foldl (fun r d => r ++ Format.line ++ formatAux ctx d) Format.nil
| ctx, node ds => Format.nest 2 $ ds.foldl (fun r d => r ++ Format.line ++ formatAux ctx d) Format.nil
instance : HasAppend MessageData := ⟨compose⟩
instance : HasFormat MessageData := ⟨fun d => formatAux none d⟩
instance : HasCoe String MessageData := ⟨fun s => ofFormat s⟩
instance coeOfFormat : HasCoe Format MessageData := ⟨ofFormat⟩
end MessageData

10
tests/lean/run/trace.lean
View file

@ -7,15 +7,15 @@ structure MyState :=
abbrev M := ReaderT Options (EState String MyState)
/- We can enable tracing for a monad M by adding an instance of `SimpleMonadTracerAdapter M` -/
instance : SimpleMonadTracerAdapter M :=
{ getOptions := read,
getTraceState := do { s ← get; pure s.traceState },
modifyTraceState := fun f =>
modify $ fun s => { traceState := f s.traceState, .. s } }
getTraceState := MyState.traceState <$> get,
modifyTraceState := fun f => modify $ fun s => { traceState := f s.traceState, .. s } }
def tst1 : M Unit :=
do trace `module (fun _ => ("hello" : MessageData));
trace `module (fun _ => ("world" : MessageData));
do trace `module (fun _ => ("hello" ++ MessageData.nest 9 (Format.line ++ "world" : MessageData)));
trace `module (fun _ => ("another message" : MessageData));
pure ()
def tst2 (b : Bool) : M Unit :=