ModuleAgda-2.7.0.1Haskell2010

Agda.Syntax.Concrete.Glyph

Choice of Unicode or ASCII glyphs.

datadata UnicodeOrAscii

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

Instances10Bounded, Enum, Eq, Show, Generic, NFData, …

Bounded UnicodeOrAsciiDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Glyph
Enum UnicodeOrAsciiDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Glyph
Eq UnicodeOrAsciiDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Glyph
Show UnicodeOrAsciiDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Glyph
Generic UnicodeOrAsciiDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Glyph
NFData UnicodeOrAsciiDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Glyph
Boolean UnicodeOrAsciiDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Glyph
IsBool UnicodeOrAsciiDefined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Glyph
EmbPrj UnicodeOrAsciiDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Errors · orphan
type Rep UnicodeOrAscii = D1 ('MetaData "UnicodeOrAscii" "Agda.Syntax.Concrete.Glyph" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) U1 :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) U1)Defined in Agda-2.7.0.1 · Agda.Syntax.Concrete.Glyph

valueunsafeSetUnicodeOrAscii :: UnicodeOrAscii -> IO ()

valuespecialCharactersForGlyphs :: UnicodeOrAscii -> SpecialCharacters

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

valuebraces' :: Doc -> Doc

valuedbraces :: Doc -> Doc

valueforallQ :: Doc

valueleftIdiomBrkt :: Doc

valuerightIdiomBrkt :: Doc

valueemptyIdiomBrkt :: Doc

valuearrow :: Doc

valuelambda :: Doc

datadata SpecialCharacters

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