Module fungi_lang::decide
[−]
[src]
Decision procedures for Fungi type and effect system.
Modules
apart |
Decide apartness of two terms (indices, name terms) |
effect |
Decide effect relationships |
equiv |
Decide equivalence of two terms (types, indices, name terms) |
subset |
Decide subset relationships over name sets, index terms and types |
Structs
Dec |
Derivation for a decision procedure, expressed as deductive inference rules |
Enums
DecError |
Decision-related error |
HandSide |
Each relation has two sides, which we refer to as |
RelCtx |
Relational typing context: Relates pairs of variables, terms, etc |
Functions
ctxs_of_relctx |
Convert the context into the corresponding relational context |
ctxs_of_relctx_rec |
Convert the context into the corresponding relational context |
relctx_of_ctx |
Convert the relational context into the corresponding non-relational context |
Type Definitions
RelCtxRec | |
Var2 |
Pair of related variables |