Agda-2.6.5: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

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 #

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.5-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 #

NFData MimerResult Source # 
Instance details

Defined in Agda.Mimer.Mimer

Methods

rnf :: MimerResult -> () #

type Rep MimerResult Source # 
Instance details

Defined in Agda.Mimer.Mimer

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