cryptol-2.6.0: Cryptol: The Language of Cryptography

Safe Haskell | Safe
Language | Haskell2010

Cryptol.Prims.Syntax

Synopsis

- data PrimTy = PrimTy {
  - primTyCon :: !TCon
  - primTyIdent :: !Ident
  - primTyDoc :: !String
  - primTyFixity :: !(Maybe Fixity)
  }
- primTyList :: [PrimTy]
- primTyIx :: Ord a => (PrimTy -> Maybe a) -> a -> Maybe PrimTy
- primTyFromPName :: PName -> Maybe PrimTy
- primTyFromTC :: TCon -> Maybe PrimTy
- primTyFromTF :: TFun -> Maybe PrimTy
- primTyFromPC :: PC -> Maybe PrimTy
- data Kind
  - = KType
  - | KNum
  - | KProp
  - | Kind :-> Kind
- class HasKind t where
  - kindOf :: t -> Kind
- data TCon
  - = TC TC
  - | PC PC
  - | TF TFun
  - | TError Kind TCErrorMessage
- data PC
  - = PEqual
  - | PNeq
  - | PGeq
  - | PFin
  - | PHas Selector
  - | PZero
  - | PLogic
  - | PArith
  - | PCmp
  - | PSignedCmp
  - | PLiteral
  - | PAnd
  - | PTrue
- data TC
  - = TCNum Integer
  - | TCInf
  - | TCBit
  - | TCInteger
  - | TCIntMod
  - | TCSeq
  - | TCFun
  - | TCTuple Int
  - | TCNewtype UserTC
- data UserTC = UserTC Name Kind
- data TCErrorMessage = TCErrorMessage {
  - tcErrorMessage :: !String
  }
- data TFun
  - = TCAdd
  - | TCSub
  - | TCMul
  - | TCDiv
  - | TCMod
  - | TCExp
  - | TCWidth
  - | TCMin
  - | TCMax
  - | TCCeilDiv
  - | TCCeilMod
  - | TCLenFromThen
  - | TCLenFromThenTo

# Documentation

data PrimTy Source #

Information about a user visible built-in type.

Constructors

PrimTy |

Fields

- primTyCon :: !TCon

  Use this ty-con (renamer)

- primTyIdent :: !Ident

  This is what it's called

- primTyDoc :: !String

  Documentation

- primTyFixity :: !(Maybe Fixity)

  Precedence, for infix ones

Instances

Eq PrimTy Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods (==) :: PrimTy -> PrimTy -> Bool Source # (/=) :: PrimTy -> PrimTy -> Bool Source #
Ord PrimTy Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods compare :: PrimTy -> PrimTy -> Ordering Source # (<) :: PrimTy -> PrimTy -> Bool Source # (<=) :: PrimTy -> PrimTy -> Bool Source # (>) :: PrimTy -> PrimTy -> Bool Source # (>=) :: PrimTy -> PrimTy -> Bool Source # max :: PrimTy -> PrimTy -> PrimTy Source # min :: PrimTy -> PrimTy -> PrimTy Source #

primTyList :: [PrimTy] Source #

This list should contain all user-visible built-in types.

primTyIx :: Ord a => (PrimTy -> Maybe a) -> a -> Maybe PrimTy Source #

Construct an index for quick lookup of primtys.

primTyFromPName :: PName -> Maybe PrimTy Source #

Lookup a prim type by a parser name.

primTyFromTC :: TCon -> Maybe PrimTy Source #

Lookup if a ty con is a primitive.

primTyFromTF :: TFun -> Maybe PrimTy Source #

Lookup a `TFun` prim type.

primTyFromPC :: PC -> Maybe PrimTy Source #

Lookup a `TCon` prim type.

data Kind Source #

Kinds, classify types.

Constructors

KType |
KNum |
KProp |
Kind :-> Kind infixr 5 |

Instances

Eq Kind Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods (==) :: Kind -> Kind -> Bool Source # (/=) :: Kind -> Kind -> Bool Source #
Ord Kind Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods compare :: Kind -> Kind -> Ordering Source # (<) :: Kind -> Kind -> Bool Source # (<=) :: Kind -> Kind -> Bool Source # (>) :: Kind -> Kind -> Bool Source # (>=) :: Kind -> Kind -> Bool Source # max :: Kind -> Kind -> Kind Source # min :: Kind -> Kind -> Kind Source #
Show Kind Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods showsPrec :: Int -> Kind -> ShowS Source # show :: Kind -> String Source # showList :: [Kind] -> ShowS Source #
Generic Kind Source # |
Instance details Defined in Cryptol.Prims.Syntax Associated Types type Rep Kind :: Type -> Type Source # Methods from :: Kind -> Rep Kind x Source # to :: Rep Kind x -> Kind Source #
NFData Kind Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods rnf :: Kind -> () Source #
PP Kind Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods ppPrec :: Int -> Kind -> Doc Source #
type Rep Kind Source # |

Instance details

Defined in Cryptol.Prims.Syntax

type Rep Kind = D1 (MetaData "Kind" "Cryptol.Prims.Syntax" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" False) ((C1 (MetaCons "KType" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "KNum" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "KProp" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons ":->" (InfixI RightAssociative 5) False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind))))

class HasKind t where Source #

Methods

kindOf :: t -> Kind Source #

Instances

HasKind TFun Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods kindOf :: TFun -> Kind Source #
HasKind UserTC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods kindOf :: UserTC -> Kind Source #
HasKind TC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods kindOf :: TC -> Kind Source #
HasKind PC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods kindOf :: PC -> Kind Source #
HasKind TCon Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods kindOf :: TCon -> Kind Source #
HasKind Newtype Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: Newtype -> Kind Source #
HasKind TySyn Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TySyn -> Kind Source #
HasKind TVar Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TVar -> Kind Source #
HasKind Type Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: Type -> Kind Source #
HasKind TParam Source # |
Instance details Defined in Cryptol.TypeCheck.Type Methods kindOf :: TParam -> Kind Source #

data TCon Source #

Type constants.

Constructors

TC TC |
PC PC |
TF TFun |
TError Kind TCErrorMessage |

Instances

Eq TCon Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods (==) :: TCon -> TCon -> Bool Source # (/=) :: TCon -> TCon -> Bool Source #
Ord TCon Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods compare :: TCon -> TCon -> Ordering Source # (<) :: TCon -> TCon -> Bool Source # (<=) :: TCon -> TCon -> Bool Source # (>) :: TCon -> TCon -> Bool Source # (>=) :: TCon -> TCon -> Bool Source # max :: TCon -> TCon -> TCon Source # min :: TCon -> TCon -> TCon Source #
Show TCon Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods showsPrec :: Int -> TCon -> ShowS Source # show :: TCon -> String Source # showList :: [TCon] -> ShowS Source #
Generic TCon Source # |
Instance details Defined in Cryptol.Prims.Syntax Associated Types type Rep TCon :: Type -> Type Source # Methods from :: TCon -> Rep TCon x Source # to :: Rep TCon x -> TCon Source #
NFData TCon Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods rnf :: TCon -> () Source #
PPName TCon Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods ppNameFixity :: TCon -> Maybe (Assoc, Int) Source # ppPrefixName :: TCon -> Doc Source # ppInfixName :: TCon -> Doc Source #
PP TCon Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods ppPrec :: Int -> TCon -> Doc Source #
HasKind TCon Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods kindOf :: TCon -> Kind Source #
FreeVars TCon Source # |
Instance details Defined in Cryptol.IR.FreeVars Methods freeVars :: TCon -> Deps Source #
type Rep TCon Source # |

Instance details

Defined in Cryptol.Prims.Syntax

type Rep TCon = D1 (MetaData "TCon" "Cryptol.Prims.Syntax" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" False) ((C1 (MetaCons "TC" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TC)) :+: C1 (MetaCons "PC" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 PC))) :+: (C1 (MetaCons "TF" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TFun)) :+: C1 (MetaCons "TError" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 TCErrorMessage))))

data PC Source #

Predicate symbols. If you add additional user-visible constructors, please update `primTys`.

Constructors

PEqual

    _ == _

PNeq

    _ /= _

PGeq

    _ >= _

PFin

    fin _

PHas Selector | `Has sel type field` does not appear in schemas

PZero

    Zero _

PLogic

    Logic _

PArith

    Arith _

PCmp

    Cmp _

PSignedCmp

    SignedCmp _

PLiteral

    Literal _ _

PAnd | This is useful when simplifying things in place
PTrue | Ditto

Instances

Eq PC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods (==) :: PC -> PC -> Bool Source # (/=) :: PC -> PC -> Bool Source #
Ord PC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods compare :: PC -> PC -> Ordering Source # (<) :: PC -> PC -> Bool Source # (<=) :: PC -> PC -> Bool Source # (>) :: PC -> PC -> Bool Source # (>=) :: PC -> PC -> Bool Source # max :: PC -> PC -> PC Source # min :: PC -> PC -> PC Source #
Show PC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods showsPrec :: Int -> PC -> ShowS Source # show :: PC -> String Source # showList :: [PC] -> ShowS Source #
Generic PC Source # |
Instance details Defined in Cryptol.Prims.Syntax Associated Types type Rep PC :: Type -> Type Source # Methods from :: PC -> Rep PC x Source # to :: Rep PC x -> PC Source #
NFData PC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods rnf :: PC -> () Source #
PP PC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods ppPrec :: Int -> PC -> Doc Source #
HasKind PC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods kindOf :: PC -> Kind Source #
type Rep PC Source # |

Instance details

Defined in Cryptol.Prims.Syntax

type Rep PC = D1 (MetaData "PC" "Cryptol.Prims.Syntax" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" False) (((C1 (MetaCons "PEqual" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "PNeq" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "PGeq" PrefixI False) (U1 :: Type -> Type))) :+: (C1 (MetaCons "PFin" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "PHas" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Selector)) :+: C1 (MetaCons "PZero" PrefixI False) (U1 :: Type -> Type)))) :+: ((C1 (MetaCons "PLogic" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "PArith" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "PCmp" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "PSignedCmp" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "PLiteral" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "PAnd" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "PTrue" PrefixI False) (U1 :: Type -> Type)))))

data TC Source #

1-1 constants. If you add additional user-visible constructors, please update `primTys`.

Constructors

TCNum Integer | Numbers
TCInf | Inf
TCBit | Bit
TCInteger | Integer

TCIntMod

    Z _

TCSeq

    [_] _

TCFun

    _ -> _

TCTuple Int

    (_, _, _)

TCNewtype UserTC | user-defined, `T`

Instances

Eq TC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods (==) :: TC -> TC -> Bool Source # (/=) :: TC -> TC -> Bool Source #
Ord TC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods compare :: TC -> TC -> Ordering Source # (<) :: TC -> TC -> Bool Source # (<=) :: TC -> TC -> Bool Source # (>) :: TC -> TC -> Bool Source # (>=) :: TC -> TC -> Bool Source # max :: TC -> TC -> TC Source # min :: TC -> TC -> TC Source #
Show TC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods showsPrec :: Int -> TC -> ShowS Source # show :: TC -> String Source # showList :: [TC] -> ShowS Source #
Generic TC Source # |
Instance details Defined in Cryptol.Prims.Syntax Associated Types type Rep TC :: Type -> Type Source # Methods from :: TC -> Rep TC x Source # to :: Rep TC x -> TC Source #
NFData TC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods rnf :: TC -> () Source #
PP TC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods ppPrec :: Int -> TC -> Doc Source #
HasKind TC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods kindOf :: TC -> Kind Source #
type Rep TC Source # |

Instance details

Defined in Cryptol.Prims.Syntax

type Rep TC = D1 (MetaData "TC" "Cryptol.Prims.Syntax" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" False) (((C1 (MetaCons "TCNum" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Integer)) :+: C1 (MetaCons "TCInf" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "TCBit" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TCInteger" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "TCIntMod" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TCSeq" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "TCFun" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "TCTuple" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Int)) :+: C1 (MetaCons "TCNewtype" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 UserTC))))))

data UserTC Source #

Constructors

UserTC Name Kind |

Instances

Eq UserTC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods (==) :: UserTC -> UserTC -> Bool Source # (/=) :: UserTC -> UserTC -> Bool Source #
Ord UserTC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods compare :: UserTC -> UserTC -> Ordering Source # (<) :: UserTC -> UserTC -> Bool Source # (<=) :: UserTC -> UserTC -> Bool Source # (>) :: UserTC -> UserTC -> Bool Source # (>=) :: UserTC -> UserTC -> Bool Source # max :: UserTC -> UserTC -> UserTC Source # min :: UserTC -> UserTC -> UserTC Source #
Show UserTC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods showsPrec :: Int -> UserTC -> ShowS Source # show :: UserTC -> String Source # showList :: [UserTC] -> ShowS Source #
Generic UserTC Source # |
Instance details Defined in Cryptol.Prims.Syntax Associated Types type Rep UserTC :: Type -> Type Source # Methods from :: UserTC -> Rep UserTC x Source # to :: Rep UserTC x -> UserTC Source #
NFData UserTC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods rnf :: UserTC -> () Source #
PP UserTC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods ppPrec :: Int -> UserTC -> Doc Source #
HasKind UserTC Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods kindOf :: UserTC -> Kind Source #
type Rep UserTC Source # |

Instance details

Defined in Cryptol.Prims.Syntax

type Rep UserTC = D1 (MetaData "UserTC" "Cryptol.Prims.Syntax" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" False) (C1 (MetaCons "UserTC" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Name) :*: S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (Rec0 Kind)))

data TCErrorMessage Source #

Constructors

TCErrorMessage |

Fields

- tcErrorMessage :: !String

Instances

Eq TCErrorMessage Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods (==) :: TCErrorMessage -> TCErrorMessage -> Bool Source # (/=) :: TCErrorMessage -> TCErrorMessage -> Bool Source #
Ord TCErrorMessage Source # |

Instance details

Defined in Cryptol.Prims.Syntax

Methods

compare :: TCErrorMessage -> TCErrorMessage -> Ordering Source #

(<) :: TCErrorMessage -> TCErrorMessage -> Bool Source #

(<=) :: TCErrorMessage -> TCErrorMessage -> Bool Source #

(>) :: TCErrorMessage -> TCErrorMessage -> Bool Source #

(>=) :: TCErrorMessage -> TCErrorMessage -> Bool Source #

max :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage Source #

min :: TCErrorMessage -> TCErrorMessage -> TCErrorMessage Source #

Show TCErrorMessage Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods showsPrec :: Int -> TCErrorMessage -> ShowS Source # show :: TCErrorMessage -> String Source # showList :: [TCErrorMessage] -> ShowS Source #
Generic TCErrorMessage Source # |
Instance details Defined in Cryptol.Prims.Syntax Associated Types type Rep TCErrorMessage :: Type -> Type Source # Methods from :: TCErrorMessage -> Rep TCErrorMessage x Source # to :: Rep TCErrorMessage x -> TCErrorMessage Source #
NFData TCErrorMessage Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods rnf :: TCErrorMessage -> () Source #
PP TCErrorMessage Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods ppPrec :: Int -> TCErrorMessage -> Doc Source #
type Rep TCErrorMessage Source # |
Instance details Defined in Cryptol.Prims.Syntax type Rep TCErrorMessage = D1 (MetaData "TCErrorMessage" "Cryptol.Prims.Syntax" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" False) (C1 (MetaCons "TCErrorMessage" PrefixI True) (S1 (MetaSel (Just "tcErrorMessage") NoSourceUnpackedness SourceStrict DecidedStrict) (Rec0 String)))

data TFun Source #

Built-in type functions. If you add additional user-visible constructors, please update `primTys` in Cryptol.Prims.Types.

Constructors

TCAdd

     : Num -> Num -> Num

TCSub

     : Num -> Num -> Num

TCMul

     : Num -> Num -> Num

TCDiv

     : Num -> Num -> Num

TCMod

     : Num -> Num -> Num

TCExp

     : Num -> Num -> Num

TCWidth

     : Num -> Num

TCMin

     : Num -> Num -> Num

TCMax

     : Num -> Num -> Num

TCCeilDiv

     : Num -> Num -> Num

TCCeilMod

     : Num -> Num -> Num

TCLenFromThen | `: Num -> Num -> Num -> Num` Example: `[ 1, 5 .. ] :: [lengthFromThen 1 5 b][b]`
TCLenFromThenTo | `: Num -> Num -> Num -> Num` Example: `[ 1, 5 .. 9 ] :: [lengthFromThenTo 1 5 9][b]`

Instances

Bounded TFun Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods minBound :: TFun Source # maxBound :: TFun Source #
Enum TFun Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods succ :: TFun -> TFun Source # pred :: TFun -> TFun Source # toEnum :: Int -> TFun Source # fromEnum :: TFun -> Int Source # enumFrom :: TFun -> [TFun] Source # enumFromThen :: TFun -> TFun -> [TFun] Source # enumFromTo :: TFun -> TFun -> [TFun] Source # enumFromThenTo :: TFun -> TFun -> TFun -> [TFun] Source #
Eq TFun Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods (==) :: TFun -> TFun -> Bool Source # (/=) :: TFun -> TFun -> Bool Source #
Ord TFun Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods compare :: TFun -> TFun -> Ordering Source # (<) :: TFun -> TFun -> Bool Source # (<=) :: TFun -> TFun -> Bool Source # (>) :: TFun -> TFun -> Bool Source # (>=) :: TFun -> TFun -> Bool Source # max :: TFun -> TFun -> TFun Source # min :: TFun -> TFun -> TFun Source #
Show TFun Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods showsPrec :: Int -> TFun -> ShowS Source # show :: TFun -> String Source # showList :: [TFun] -> ShowS Source #
Generic TFun Source # |
Instance details Defined in Cryptol.Prims.Syntax Associated Types type Rep TFun :: Type -> Type Source # Methods from :: TFun -> Rep TFun x Source # to :: Rep TFun x -> TFun Source #
NFData TFun Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods rnf :: TFun -> () Source #
PPName TFun Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods ppNameFixity :: TFun -> Maybe (Assoc, Int) Source # ppPrefixName :: TFun -> Doc Source # ppInfixName :: TFun -> Doc Source #
PP TFun Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods ppPrec :: Int -> TFun -> Doc Source #
HasKind TFun Source # |
Instance details Defined in Cryptol.Prims.Syntax Methods kindOf :: TFun -> Kind Source #
type Rep TFun Source # |

Instance details

Defined in Cryptol.Prims.Syntax

type Rep TFun = D1 (MetaData "TFun" "Cryptol.Prims.Syntax" "cryptol-2.6.0-FO78l5UWBYr51eDL1ksQpO" False) (((C1 (MetaCons "TCAdd" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "TCSub" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TCMul" PrefixI False) (U1 :: Type -> Type))) :+: (C1 (MetaCons "TCDiv" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "TCMod" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TCExp" PrefixI False) (U1 :: Type -> Type)))) :+: ((C1 (MetaCons "TCWidth" PrefixI False) (U1 :: Type -> Type) :+: (C1 (MetaCons "TCMin" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TCMax" PrefixI False) (U1 :: Type -> Type))) :+: ((C1 (MetaCons "TCCeilDiv" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TCCeilMod" PrefixI False) (U1 :: Type -> Type)) :+: (C1 (MetaCons "TCLenFromThen" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "TCLenFromThenTo" PrefixI False) (U1 :: Type -> Type)))))