Module fungi_lang::decide

Expand description

Decision procedures for Fungi type and effect system.

Modules

Decide apartness of two terms (indices, name terms)

Decide effect relationships

Decide equivalence of two terms (types, indices, name terms)

Decide subset relationships over name sets, index terms and types

Derivation for a decision procedure, expressed as deductive inference rules

Decision-related error

Each relation has two sides, which we refer to as L and R

Relational typing context: Relates pairs of variables, terms, etc

Convert the context into the corresponding relational context

Convert the context into the corresponding relational context

Convert the relational context into the corresponding non-relational context

Pair of related variables