flux_infer::fixpoint_encoding

Module fixpoint

Source

Re-exports§

pub use fixpoint_generated::*;

Modules§

fixpoint_generated

Structs§

AdtId
Unique id assigned to each flux_middle::rty::AdtSortDef that needs to be encoded into fixpoint
GlobalVar
KVid
LocalVar
SymStr

Enums§

DataSort
Var