@@ -1806,8 +1806,9 @@ reflectName (MN i n)
18061806reflectName (NErased) = Var (reflm "NErased")
18071807reflectName n = Var (reflm "NErased") -- special name, not yet implemented
18081808
1809−-- | Elaborate a name to a pattern. This means that NS and UN will be intact,
1810−-- while all others become _
1809+-- | Elaborate a name to a pattern. This means that NS and UN will be intact.
1810+-- MNs corresponding to will care about the string but not the number. All
1811+-- others become _.
18111812reflectNameQuotePattern :: Name -> ElabD ()
18121813reflectNameQuotePattern n@(UN s)
18131814 = do fill $ reflectName n
@@ -1815,6 +1816,12 @@ reflectNameQuotePattern n@(UN s)
18151816reflectNameQuotePattern n@(NS _ _)
18161817 = do fill $ reflectName n
18171818 solve
1819+reflectNameQuotePattern (MN _ n)
1820+ = do i <- getNameFrom (sMN 0 "mnCounter")
1821+ claim i (RConstant (AType (ATInt ITNative)))
1822+ movelast i
1823+ fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]
1824+ solve
18181825reflectNameQuotePattern _ -- for all other names, match any
18191826 = do nameHole <- getNameFrom (sMN 0 "name")
18201827 claim nameHole (Var (reflm "TTName"))