Module fungi_lang::decide

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 L and R
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