Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Syntax.Concrete.Glyph

Description

Choice of Unicode or ASCII glyphs.

Synopsis

- data UnicodeOrAscii
  - = UnicodeOk
  - | AsciiOnly
- unsafeSetUnicodeOrAscii :: UnicodeOrAscii -> IO ()
- specialCharactersForGlyphs :: UnicodeOrAscii -> SpecialCharacters
- braces' :: Doc -> Doc
- dbraces :: Doc -> Doc
- forallQ :: Doc
- leftIdiomBrkt :: Doc
- rightIdiomBrkt :: Doc
- emptyIdiomBrkt :: Doc
- arrow :: Doc
- lambda :: Doc
- data SpecialCharacters = SpecialCharacters {
  - _dbraces :: Doc -> Doc
  - _lambda :: Doc
  - _arrow :: Doc
  - _forallQ :: Doc
  - _leftIdiomBrkt :: Doc
  - _rightIdiomBrkt :: Doc
  - _emptyIdiomBrkt :: Doc
  }

# 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 Word32 Source # icod_ :: UnicodeOrAscii -> S Word32 Source # value :: Word32 -> 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 -> () Source #
Bounded UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods minBound :: UnicodeOrAscii Source # maxBound :: UnicodeOrAscii Source #
Enum UnicodeOrAscii Source # |

Instance details

Defined in Agda.Syntax.Concrete.Glyph

Methods

succ :: UnicodeOrAscii -> UnicodeOrAscii Source #

pred :: UnicodeOrAscii -> UnicodeOrAscii Source #

toEnum :: Int -> UnicodeOrAscii Source #

fromEnum :: UnicodeOrAscii -> Int Source #

enumFrom :: UnicodeOrAscii -> [UnicodeOrAscii] Source #

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

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

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

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.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "UnicodeOk" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "AsciiOnly" 'PrefixI 'False) (U1 :: Type -> Type))

Methods

from :: UnicodeOrAscii -> Rep UnicodeOrAscii x Source #

to :: Rep UnicodeOrAscii x -> UnicodeOrAscii Source #

Show UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods showsPrec :: Int -> UnicodeOrAscii -> ShowS Source # show :: UnicodeOrAscii -> String Source # showList :: [UnicodeOrAscii] -> ShowS Source #
Eq UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph Methods (==) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool Source # (/=) :: UnicodeOrAscii -> UnicodeOrAscii -> Bool Source #
type Rep UnicodeOrAscii Source # |
Instance details Defined in Agda.Syntax.Concrete.Glyph type Rep UnicodeOrAscii = D1 ('MetaData "UnicodeOrAscii" "Agda.Syntax.Concrete.Glyph" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" '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

- _dbraces :: Doc -> Doc
- _lambda :: Doc
- _arrow :: Doc
- _forallQ :: Doc
- _leftIdiomBrkt :: Doc
- _rightIdiomBrkt :: Doc
- _emptyIdiomBrkt :: Doc