Agda-2.6.2.1: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Syntax.Concrete.Glyph

Description

Choice of Unicode or ASCII glyphs.

Synopsis

Documentation

data UnicodeOrAscii Source #

We want to know whether we are allowed to insert unicode characters or not.

Constructors

UnicodeOk 
AsciiOnly 

Instances

Instances details
EmbPrj UnicodeOrAscii Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Errors

Methods

icode :: UnicodeOrAscii -> S Int32 Source #

icod_ :: UnicodeOrAscii -> S Int32 Source #

value :: Int32 -> R UnicodeOrAscii Source #

Bounded UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

minBound :: UnicodeOrAscii #

maxBound :: UnicodeOrAscii #

Enum UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

succ :: UnicodeOrAscii -> UnicodeOrAscii #

pred :: UnicodeOrAscii -> UnicodeOrAscii #

toEnum :: Int -> UnicodeOrAscii #

fromEnum :: UnicodeOrAscii -> Int #

enumFrom :: UnicodeOrAscii -> [UnicodeOrAscii] #

enumFromThen :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] #

enumFromTo :: UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] #

enumFromThenTo :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii -> [UnicodeOrAscii] #

Generic UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Associated Types

type Rep UnicodeOrAscii :: Type -> Type #

Methods

from :: UnicodeOrAscii -> Rep UnicodeOrAscii x #

to :: Rep UnicodeOrAscii x -> UnicodeOrAscii #

Show UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

showsPrec :: Int -> UnicodeOrAscii -> ShowS #

show :: UnicodeOrAscii -> String #

showList :: [UnicodeOrAscii] -> ShowS #

NFData UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

rnf :: UnicodeOrAscii -> () #

Eq UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

(==) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool #

(/=) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool #

type Rep UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

type Rep UnicodeOrAscii = D1 ('MetaData "UnicodeOrAscii" "Agda.Syntax.Concrete.Glyph" "Agda-2.6.2.1-inplace" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) (U1 :: Type -> Type))

unsafeSetUnicodeOrAscii :: UnicodeOrAscii -> IO () Source #

specialCharactersForGlyphs :: UnicodeOrAscii -> SpecialCharacters Source #

Return the glyph set based on a given (unicode or ascii) glyph mode

braces' :: Doc -> Doc Source #

dbraces :: Doc -> Doc Source #

forallQ :: Doc Source #

leftIdiomBrkt :: Doc Source #

rightIdiomBrkt :: Doc Source #

emptyIdiomBrkt :: Doc Source #

arrow :: Doc Source #

lambda :: Doc Source #

data SpecialCharacters Source #

Picking the appropriate set of special characters depending on whether we are allowed to use unicode or have to limit ourselves to ascii.

Constructors

SpecialCharacters 

Fields