Module fixpoint 

Re-exports

pub use fixpoint_generated::*;

Modules

fixpoint_generated

Structs

AdtId

Unique id assigned to each [rty::AdtSortDef] that needs to be encoded into fixpoint

GlobalVar

KVid

LocalVar

OpaqueId

Unique id assigned to each opaque/user sort that needs to be encoded into fixpoint (see DataSort::User(OpaqueId) and declare_opaque_sort)

SymStr

Enums

DataSort

Var