feat(delate): Add mdata annotation for matcher
This commit is contained in:
parent
a28ad9b239
commit
3b4b196a30
|
@ -170,7 +170,8 @@ def instantiateAll (e: Expr): MetaM Expr := do
|
|||
| .some mapp =>
|
||||
let .some matcherInfo := (← getEnv).find? mapp.matcherName | panic! "Matcher must exist"
|
||||
let f ← Meta.instantiateValueLevelParams matcherInfo mapp.matcherLevels.toList
|
||||
return .visit (f.betaRev e'.getAppRevArgs (useZeta := true))
|
||||
let mdata := KVMap.empty.insert `matcher (DataValue.ofName mapp.matcherName)
|
||||
return .visit $ .mdata mdata (f.betaRev e'.getAppRevArgs (useZeta := true))
|
||||
return e
|
||||
|
||||
structure DelayedMVarInvocation where
|
||||
|
|
Loading…
Reference in New Issue