|
Ivor.ViewTerm | Portability | non-portable | Stability | experimental | Maintainer | eb@dcs.st-and.ac.uk |
|
|
|
|
|
Description |
Exported view of terms and inductive data structures; imported
implicitly by Ivor.TT.
|
|
Synopsis |
|
|
|
|
Variable names
|
|
|
Instances | |
|
|
|
|
|
|
|
Categories for names; typechecked terms will know what each variable
is for.
| Constructors | Bound | | Free | | DataCon | | TypeCon | | ElimOp | | Unknown | Use for sending to typechecker.
|
| Instances | |
|
|
|
:: String | Variable name
| -> ViewTerm | | Construct a term representing a variable
|
|
|
Terms
|
|
|
Abstract type representing a TT term and its type.
| Constructors | | Instances | |
|
|
|
Constructors | Name | | | App | | | Lambda | | | Forall | | | Let | | | Label | | | Call | | | Return | | | forall c . Constant c => Constant c | | Star | | Quote | Staging annotation
| | Code | Staging annotation
| | Eval | Staging annotation
| | Escape | Staging annotation
| | Placeholder | | Annotation | additional annotations
| | Metavar | | |
| Instances | |
|
|
|
Constructors | | Instances | |
|
|
|
Make an application of a function to several arguments
|
|
|
Get a pattern matchable representation of a term.
|
|
|
Get a pattern matchable representation of a term's type.
|
|
|
Haskell types which can be used as constants
| | Methods | | | Instances | |
|
|
|
Return whether the name occurs free in the term.
|
|
|
Return the names occurring free in a term
|
|
|
Return whether a subterm occurs in a (first order) term.
|
|
|
Substitute a name n with a value v in a term f
|
|
|
Get the function from an application. If no application, returns the
entire term.
|
|
|
Get the arguments from a function application.
|
|
|
:: ViewTerm | Left hand side, with metavariables
| -> ViewTerm | Right hand side, with metavariables
| -> ViewTerm | Term to rewrite
| -> ViewTerm | | Transform a term according to a rewrite rule.
|
|
|
|
Get the argument names and types from a function type
|
|
|
Get the return type from a function type
|
|
|
|
Inductive types
|
|
|
Constructors | | Instances | |
|
|
Produced by Haddock version 2.6.0 |