Module hax_paths

This module defines the ImplFnDecoration structure and utils around it.

Constants

DECORATION_KINDS

The various strings allowed as decoration kinds.

Functions

expect_simple_path 🔒

expects_hax_path

Expects a Path to be a hax path: ::hax_lib::<KW>, hax_lib::<KW> or <KW> in (with KW in allowlist).

expects_order

Expects a path to be [[::]hax_lib]::order

expects_path_decoration

Expects a Path to be a decoration kind: ::hax_lib::<KIND>, hax_lib::<KIND> or <KIND> in (with KIND in DECORATION_KINDS).

expects_refine

Expects a path to be [[::]hax_lib]::refine