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

chore: fix trace class

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-17 13:22:16 -07:00
parent 184b0b8e8d
commit 719db55a9c
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/Match/Match.lean
View file

@ -708,7 +708,7 @@ builtin_initialize matcherExt : EnvExtension (Std.PHashMap (Expr × Bool) Name)
/- Similar to `mkAuxDefinition`, but uses the cache `matcherExt`.
It also returns an Boolean that indicates whether a new matcher function was added to the environment or not. -/
def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (Expr × (Option $ MatcherInfo → MetaM Unit)) := do
trace[Meta.debug] "{name} : {type} := {value}"
trace[Meta.Match.debug] "{name} : {type} := {value}"
let compile := bootstrap.genMatcherCode.get (← getOptions)
let result ← Closure.mkValueTypeClosure type value (zeta := false)
let env ← getEnv
@ -725,7 +725,7 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (E
hints := ReducibilityHints.abbrev
safety := if env.hasUnsafe result.type || env.hasUnsafe result.value then DefinitionSafety.unsafe else DefinitionSafety.safe
}
trace[Meta.debug] "{name} : {result.type} := {result.value}"
trace[Meta.Match.debug] "{name} : {result.type} := {result.value}"
let addMatcher : MatcherInfo → MetaM Unit := fun mi => do
addDecl decl
modifyEnv fun env => matcherExt.modifyState env fun s => s.insert (result.value, compile) name