Module wf

Checks type well-formedness

Well-formedness checking assumes names are correctly bound which is guaranteed after desugaring.

Modules

errors 🔒

param_usage 🔒

Code to check whether refinement parameters are used in allowed positions.

sortck 🔒

Structs

RefineParamVisitor 🔒

Wf 🔒

Functions

check_constant_expr 🔒

check_flux_item 🔒

check_invariants 🔒

check_node 🔒

visit_refine_params 🔒

Type Aliases

Result 🔒