Crate flux_middle

source ·
Expand description

This crate contains common type definitions that are used by other crates.

Modules§

  • big_int
  • cstore
  • fhir
    Flux High-Level Intermediate Representation
  • global_env
  • pretty
  • queries
  • rty
    Defines how flux represents refinement types internally. Definitions in this module are used during refinement type checking. A couple of important differences between definitions in this module and in crate::fhir are:
  • sort_of 🔒

Macros§

Structs§

Enums§

  • ExternSpecMappingErr
    Represents errors that can occur when inserting a mapping between a LocalDefId and a DefId for an extern spec.
  • MaybeExternId
    This enum serves as a type-level reminder that a local definition may be a wrapper for an extern spec. This abstraction is not infallible, so one should be careful and decide in each situation whether to use the local id or the resolved id.
  • ResolvedDefId
    Normally, a DefId is either local or external, and DefId::as_local can be used to distinguish between the two. However, extern specs introduce a third case: a local definition wrapping an extern spec. This enum is a type level reminder used to differentiate between these three cases.

Statics§

  • DEFAULT_LOCALE_RESOURCE
    Raw content of Fluent resource for this crate, generated by fluent_messages macro, imported by rustc_driver to include all crates’ resources in one bundle.
  • THEORY_FUNCS

Traits§

Functions§