Agda-2.5.2: A dependently typed functional programming language and proof assistant
Agda.Syntax.Literal
Synopsis
data Literal #
Constructors
Instances
Methods
(==) :: Literal -> Literal -> Bool #
(/=) :: Literal -> Literal -> Bool #
compare :: Literal -> Literal -> Ordering #
(<) :: Literal -> Literal -> Bool #
(<=) :: Literal -> Literal -> Bool #
(>) :: Literal -> Literal -> Bool #
(>=) :: Literal -> Literal -> Bool #
max :: Literal -> Literal -> Literal #
min :: Literal -> Literal -> Literal #
showsPrec :: Int -> Literal -> ShowS #
show :: Literal -> String #
showList :: [Literal] -> ShowS #
Ranges are not forced.
rnf :: Literal -> () #
pretty :: Literal -> Doc #
prettyPrec :: Int -> Literal -> Doc #
killRange :: KillRangeT Literal #
setRange :: Range -> Literal -> Literal #
getRange :: Literal -> Range #
namesIn :: Literal -> Set QName #
prettyTCM :: Literal -> TCM Doc #
unquote :: Term -> UnquoteM Literal #
toAbstract :: Literal -> WithNames Expr #
reify :: Literal -> TCM Expr #
reifyWhen :: Bool -> Literal -> TCM Expr #
showString' :: String -> ShowS #
showChar' :: Char -> ShowS #
compareFloat :: Double -> Double -> Ordering #