Skip to content

HORIZON HASKELL Docs lts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

ModuleAgda-2.7.0.1Haskell2010

Agda.Mimer.Mimer

1 type
1 value

PackageAgda-2.7.0.1
Exports2
LanguageHaskell2010
LicenceMIT

datadata MimerResult

Constructors

MimerExpr String
Returns String rather than Expr because the give action expects a string.
MimerClauses QName [Clause]
MimerList [(Int, String)]
MimerNoResult

Instances4Generic, NFData, PrettyTCM, Rep

Generic MimerResultDefined in Agda-2.7.0.1 · Agda.Mimer.Mimer
NFData MimerResultDefined in Agda-2.7.0.1 · Agda.Mimer.Mimer
PrettyTCM MimerResultDefined in Agda-2.7.0.1 · Agda.Mimer.Mimer
type Rep MimerResult = D1 ('MetaData "MimerResult" "Agda.Mimer.Mimer" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) ((C1 ('MetaCons "MimerExpr" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "MimerClauses" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]))) :+: (C1 ('MetaCons "MimerList" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Int, String)])) :+: C1 ('MetaCons "MimerNoResult" 'PrefixI 'False) U1))Defined in Agda-2.7.0.1 · Agda.Mimer.Mimer

valuemimer

:: MonadTCM tcm
=> Rewrite
-> InteractionId
-> Range
-> String
-> tcm MimerResult