Agda.Mimer.Mimer

Documentation

data MimerResult

Constructors

MimerExpr String

Returns String rather than Expr because the give action expects a string.

MimerClauses QName [Clause]

MimerList [(Int, String)]

MimerNoResult

Instances

PrettyTCM MimerResult

Defined in Agda.Mimer.Mimer

Methods

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

Generic MimerResult

Defined in Agda.Mimer.Mimer

Associated Types

type Rep MimerResult :: Type -> Type

Methods

from :: MimerResult -> Rep MimerResult x

to :: Rep MimerResult x -> MimerResult

NFData MimerResult

Defined in Agda.Mimer.Mimer

Methods

rnf :: MimerResult -> ()

type Rep MimerResult

Defined in Agda.Mimer.Mimer

type Rep MimerResult = D1 ('MetaData "MimerResult" "Agda.Mimer.Mimer" "Agda-2.7.0.1-LY5YwrqyXvw4P0XfI08pJQ" '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