Agda.Syntax.Literal

Documentation

data Literal

Constructors

LitNat Range !Integer

LitWord64 Range !Word64

LitFloat Range !Double

LitString Range String

LitChar Range !Char

LitQName Range QName

LitMeta Range AbsolutePath MetaId

Instances

Eq Literal

Defined in Agda.Syntax.Literal

Methods

(==) :: Literal -> Literal -> Bool

(/=) :: Literal -> Literal -> Bool

Data Literal

Defined in Agda.Syntax.Literal

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Literal -> c Literal

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Literal

toConstr :: Literal -> Constr

dataTypeOf :: Literal -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Literal)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Literal)

gmapT :: (forall b. Data b => b -> b) -> Literal -> Literal

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Literal -> r

gmapQ :: (forall d. Data d => d -> u) -> Literal -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Literal -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Literal -> m Literal

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Literal -> m Literal

Ord Literal

Defined in Agda.Syntax.Literal

Methods

compare :: Literal -> Literal -> Ordering

(<) :: Literal -> Literal -> Bool

(<=) :: Literal -> Literal -> Bool

(>) :: Literal -> Literal -> Bool

(>=) :: Literal -> Literal -> Bool

max :: Literal -> Literal -> Literal

min :: Literal -> Literal -> Literal

Show Literal

Defined in Agda.Syntax.Literal

Methods

showsPrec :: Int -> Literal -> ShowS

show :: Literal -> String

showList :: [Literal] -> ShowS

NFData Literal

Ranges are not forced.

Defined in Agda.Syntax.Literal

Methods

rnf :: Literal -> ()

Pretty Literal

Defined in Agda.Syntax.Literal

Methods

pretty :: Literal -> Doc

prettyPrec :: Int -> Literal -> Doc

prettyList :: [Literal] -> Doc

KillRange Literal

Defined in Agda.Syntax.Literal

Methods

killRange :: KillRangeT Literal

SetRange Literal

Defined in Agda.Syntax.Literal

Methods

setRange :: Range -> Literal -> Literal

HasRange Literal

Defined in Agda.Syntax.Literal

Methods

getRange :: Literal -> Range

EmbPrj Literal

Defined in Agda.TypeChecking.Serialise.Instances.Common

Methods

icode :: Literal -> S Int32

icod_ :: Literal -> S Int32

value :: Int32 -> R Literal

PrettyTCM Literal

Defined in Agda.TypeChecking.Pretty

Methods

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

NamesIn Literal

Defined in Agda.Syntax.Internal.Names

Methods

namesIn :: Literal -> Set QName

Unquote Literal

Defined in Agda.TypeChecking.Unquote

Methods

unquote :: Term -> UnquoteM Literal

ToAbstract Literal Expr

Defined in Agda.Syntax.Translation.ReflectedToAbstract

Methods

toAbstract :: MonadReflectedToAbstract m => Literal -> m Expr

Reify Literal Expr

Defined in Agda.Syntax.Translation.InternalToAbstract

Methods

reify :: MonadReify m => Literal -> m Expr

reifyWhen :: MonadReify m => Bool -> Literal -> m Expr

showString' :: String -> ShowS

showChar' :: Char -> ShowS

compareFloat :: Double -> Double -> Ordering