Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Synopsis
- infixPrimTy :: TCon -> Maybe (Ident, Fixity)
- builtInType :: Name -> Maybe TCon
- data Kind
- class HasKind t where
- data TCon
- data PC
- data TC
- data UserTC = UserTC Name Kind
- data TCErrorMessage = TCErrorMessage {
- tcErrorMessage :: !String
- data TFun
Documentation
infixPrimTy :: TCon -> Maybe (Ident, Fixity) Source #
This is used for pretty prinitng. XXX: it would be nice to just rely in the info from the Prelude.
Kinds, classify types.
Instances
Eq Kind Source # | |
Ord Kind Source # | |
Show Kind Source # | |
Generic Kind Source # | |
NFData Kind Source # | |
Defined in Cryptol.TypeCheck.TCon | |
PP Kind Source # | |
type Rep Kind Source # | |
Defined in Cryptol.TypeCheck.TCon type Rep Kind = D1 (MetaData "Kind" "Cryptol.TypeCheck.TCon" "cryptol-2.9.1-EDtcoHURvveHmx5M6ZZjMK" 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)))) |
Type constants.
Instances
Predicate symbols.
If you add additional user-visible constructors, please update primTys
.
PEqual | _ == _ |
PNeq | _ /= _ |
PGeq | _ >= _ |
PFin | fin _ |
PHas Selector |
|
PZero | Zero _ |
PLogic | Logic _ |
PRing | Ring _ |
PIntegral | Integral _ |
PField | Field _ |
PRound | Round _ |
PEq | Eq _ |
PCmp | Cmp _ |
PSignedCmp | SignedCmp _ |
PLiteral | Literal _ _ |
PFLiteral | FLiteral _ _ _ |
PValidFloat |
|
PAnd | This is useful when simplifying things in place |
PTrue | Ditto |
Instances
1-1 constants.
If you add additional user-visible constructors, please update primTys
.
TCNum Integer | Numbers |
TCInf | Inf |
TCBit | Bit |
TCInteger | Integer |
TCFloat | Float |
TCIntMod | Z _ |
TCRational | Rational |
TCArray | Array _ _ |
TCSeq | [_] _ |
TCFun | _ -> _ |
TCTuple Int | (_, _, _) |
TCAbstract UserTC | An abstract type |
TCNewtype UserTC | user-defined, |
Instances
Instances
Eq UserTC Source # | |
Ord UserTC Source # | |
Show UserTC Source # | |
Generic UserTC Source # | |
NFData UserTC Source # | |
Defined in Cryptol.TypeCheck.TCon | |
PP UserTC Source # | |
HasKind UserTC Source # | |
type Rep UserTC Source # | |
Defined in Cryptol.TypeCheck.TCon type Rep UserTC = D1 (MetaData "UserTC" "Cryptol.TypeCheck.TCon" "cryptol-2.9.1-EDtcoHURvveHmx5M6ZZjMK" 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 #
Instances
Built-in type functions.
If you add additional user-visible constructors,
please update primTys
in Cryptol.Prims.Types.
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 |
TCLenFromThenTo |
|