| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Concrete
Contents
Synopsis
- data Name = Name {}
- data QName
- unqual :: QName -> Name
- set0 :: Expr
- ident :: Name -> Expr
- data Expr
- data LetDef = LetDef {
- letDefDec :: Dec
- letDefName :: Name
- letDefTel :: Telescope
- letDefType :: Maybe Type
- letDefExpr :: Expr
- data Declaration
- data TypeSig = TypeSig Name Type
- type Type = Expr
- data Constructor = Constructor {}
- type TBind = TBinding Type
- type LBind = TBinding (Maybe Type)
- data TBinding a
- type Telescope = [TBind]
- data DefClause = DefClause Name [Elim] (Maybe Expr)
- data Elim
- data Clause = Clause (Maybe Name) [Pattern] (Maybe Expr)
- data Pattern
- type Case = (Pattern, Expr)
- patApp :: Pattern -> [Pattern] -> Pattern
- prettyLBind :: LBind -> String
- prettyTBind :: Bool -> TBind -> String
- prettyLetBody :: String -> Expr -> String
- prettyLetAssign :: String -> Expr -> String
- prettyLetDef :: LetDef -> String
- prettyDecId :: Dec -> Name -> String
- prettyTel :: Bool -> Telescope -> String
- prettyMaybeType :: Maybe Expr -> String
- prettyExpr :: Expr -> String
- prettyRecordLine :: ([Name], Expr) -> String
- prettyCase :: Clause -> String
- prettyPattern :: Pattern -> String
- prettyExprs :: [Expr] -> String
- prettyDecl :: Declaration -> String
- teleToType :: Telescope -> Type -> Type
- typeToTele :: Type -> (Telescope, Type)
- teleNames :: Telescope -> [Name]
- tbindNames :: TBind -> [Name]
Documentation
Possibly qualified names.
Concrete expressions syntax.
Constructors
| Set Expr | Universe |
| CoSet Expr | |
| Size |
|
| Succ Expr |
|
| Zero |
|
| Infty |
|
| Max |
|
| Plus Expr Expr |
|
| RApp Expr Expr |
|
| App Expr [Expr] |
|
| Lam Name Expr |
|
| Case Expr (Maybe Type) [Clause] |
|
| LLet LetDef Expr |
|
| Quant PiSigma Telescope Expr |
|
| Pair Expr Expr |
|
| Record [([Name], Expr)] |
|
| Proj Name |
|
| Ident QName |
|
| Unknown |
|
| Sing Expr Expr |
|
Constructors
| LetDef | |
Fields
| |
data Declaration Source #
Constructors
Instances
| Show Declaration Source # | |
Defined in Concrete Methods showsPrec :: Int -> Declaration -> ShowS # show :: Declaration -> String # showList :: [Declaration] -> ShowS # | |
| Eq Declaration Source # | |
Defined in Concrete | |
data Constructor Source #
Instances
| Show Constructor Source # | |
Defined in Concrete Methods showsPrec :: Int -> Constructor -> ShowS # show :: Constructor -> String # showList :: [Constructor] -> ShowS # | |
| Eq Constructor Source # | |
Defined in Concrete | |
Constructors
| TBind | |
Fields
| |
| TBounded | |
| TMeasure (Measure Expr) | |
| TBound (Bound Expr) | |
Pretty printing.
prettyLBind :: LBind -> String Source #
prettyLetDef :: LetDef -> String Source #
prettyExpr :: Expr -> String Source #
prettyCase :: Clause -> String Source #
prettyPattern :: Pattern -> String Source #
prettyExprs :: [Expr] -> String Source #
prettyDecl :: Declaration -> String Source #
tbindNames :: TBind -> [Name] Source #