Module fungi_lang::decide [−] [src]

Decision procedures for Fungi type and effect system.

Modules

apart	Decide apartness of two terms (indices, name terms)
equiv	Decide equivalence of two terms (types, indices, name terms)

Dec	Derivation for a decision procedure, expressed as deductive inference rules

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

ctx_of_relctx	Convert the context into the corresponding relational context
relctx_of_ctx	Convert the context into the corresponding relational context