HERMIT.Dictionary.Remembered

Remembering definitions.

externals :: [External]

prefixRemembered :: LemmaName -> LemmaName

rememberR :: (AddBindings c, ExtendPath c Crumb, ReadPath c Crumb, HasLemmas m, MonadCatch m) => LemmaName -> Transform c m Core ()

Remember a binding with a name for later use. Allows us to look at past definitions.

unfoldRememberedR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasLemmas m, MonadCatch m, MonadUnique m) => Used -> LemmaName -> Rewrite c m CoreExpr

Unfold a remembered definition (like unfoldR, but looks in stash instead of context).

foldRememberedR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasLemmas m, MonadCatch m, MonadUnique m) => Used -> LemmaName -> Rewrite c m CoreExpr

Fold a remembered definition (like foldR, but looks in stash instead of context).

foldAnyRememberedR :: (AddBindings c, ExtendPath c Crumb, HasEmptyContext c, LemmaContext c, ReadBindings c, ReadPath c Crumb, HasLemmas m, MonadCatch m, MonadUnique m) => Rewrite c m CoreExpr

Fold any of the remembered definitions.

compileRememberedT :: (LemmaContext c, HasLemmas m, Monad m) => Transform c m x CompiledFold

Compile all remembered definitions into something that can be run with runFoldR