Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
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

true: Unicode characters are allowed.

AsciiOnly

'false: Stick to ASCII.

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 #

Boolean UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

fromBool :: Bool -> UnicodeOrAscii Source #

true :: UnicodeOrAscii Source #

false :: UnicodeOrAscii Source #

not :: UnicodeOrAscii -> UnicodeOrAscii Source #

(&&) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

(||) :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

implies :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

butNot :: UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

IsBool UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

toBool :: UnicodeOrAscii -> Bool Source #

ifThenElse :: UnicodeOrAscii -> b -> b -> b Source #

fromBool1 :: (Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii Source #

fromBool2 :: (Bool -> Bool -> Bool) -> UnicodeOrAscii -> UnicodeOrAscii -> UnicodeOrAscii Source #

NFData UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

rnf :: UnicodeOrAscii -> ()

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 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

type Rep UnicodeOrAscii = D1 ('MetaData "UnicodeOrAscii" "Agda.Syntax.Concrete.Glyph" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) (U1 :: 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

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.20240714-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