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

Bounded UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Enum UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Generic UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

Associated Types

type Rep UnicodeOrAscii :: Type -> Type #

Show UnicodeOrAscii Source # 
Instance details

Defined in Agda.Syntax.Concrete.Glyph

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

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))

specialCharactersForGlyphs :: UnicodeOrAscii -> SpecialCharacters Source #

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

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.