Agda-2.5.3: A dependently typed functional programming language and proof assistant

Safe Haskell	None
Language	Haskell2010

Agda.Syntax.Literal

Synopsis

Documentation

Constructors

LitNat Range !Integer
LitFloat Range !Double
LitString Range String
LitChar Range !Char
LitQName Range QName
LitMeta Range AbsolutePath MetaId

Instances

Eq Literal #
Methods (==) :: Literal -> Literal -> Bool # (/=) :: Literal -> Literal -> Bool #
Data 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 #
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 #
Methods showsPrec :: Int -> Literal -> ShowS # show :: Literal -> String # showList :: [Literal] -> ShowS #
NFData Literal #	Ranges are not forced.
Methods rnf :: Literal -> () #
Pretty Literal #
Methods pretty :: Literal -> Doc # prettyPrec :: Int -> Literal -> Doc # prettyList :: [Literal] -> Doc #
KillRange Literal #
Methods killRange :: KillRangeT Literal #
SetRange Literal #
Methods setRange :: Range -> Literal -> Literal #
HasRange Literal #
Methods getRange :: Literal -> Range #
PrettyTCM Literal #
Methods prettyTCM :: Literal -> TCM Doc #
NamesIn Literal #
Methods namesIn :: Literal -> Set QName #
Unquote Literal #
Methods unquote :: Term -> UnquoteM Literal #
Reify Literal Expr #
Methods reify :: Literal -> TCM Expr # reifyWhen :: Bool -> Literal -> TCM Expr #
ToAbstract Literal Expr #
Methods toAbstract :: Literal -> WithNames Expr #

showString' :: String -> ShowS #

showChar' :: Char -> ShowS #

compareFloat :: Double -> Double -> Ordering #