Safe Haskell	None
Language	Haskell2010

Agda.Mimer.Mimer

Documentation

data MimerResult Source #

Constructors

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

Instances

Instances details

PrettyTCM MimerResult Source #

Instance details

Defined in Agda.Mimer.Mimer

Methods

prettyTCM :: MonadPretty m => MimerResult -> m Doc Source #

NFData MimerResult Source #

Instance details

Defined in Agda.Mimer.Mimer

Methods

rnf :: MimerResult -> ()

Generic MimerResult Source #

Instance details

Defined in Agda.Mimer.Mimer

Associated Types

type Rep MimerResult

Instance details

Defined in Agda.Mimer.Mimer

type Rep MimerResult = D1 ('MetaData "MimerResult" "Agda.Mimer.Mimer" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "MimerExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "MimerClauses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]))) :+: (C1 ('MetaCons "MimerList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Int, String)])) :+: C1 ('MetaCons "MimerNoResult" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: MimerResult -> Rep MimerResult x

to :: Rep MimerResult x -> MimerResult

type Rep MimerResult Source #

Instance details

Defined in Agda.Mimer.Mimer

type Rep MimerResult = D1 ('MetaData "MimerResult" "Agda.Mimer.Mimer" "Agda-2.6.20240714-inplace" 'False) ((C1 ('MetaCons "MimerExpr" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String)) :+: C1 ('MetaCons "MimerClauses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 QName) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Clause]))) :+: (C1 ('MetaCons "MimerList" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [(Int, String)])) :+: C1 ('MetaCons "MimerNoResult" 'PrefixI 'False) (U1 :: Type -> Type)))

mimer :: MonadTCM tcm => Rewrite -> InteractionId -> Range -> String -> tcm MimerResult Source #