Crate liquid_fixpoint 

This crate implements an interface to the liquid-fixpoint binary

Modules

constraint 🔒

constraint_with_env 🔒

format 🔒

parser 🔒

sexp 🔒

Macros

declare_types

Structs

Bind

ConstDecl

CrashInfo

DataCtor

DataDecl

DataField

Error

ErrorInner 🔒

FunDef

KVarDecl

Qualifier

Stats

Task

Enums

BinOp

BinRel

Constant

Constraint

Expr

FixpointResult

Pred

SmtSolver

Sort

SortCtor

ThyFunc

Traits

FixpointFmt

Identifier

Types

Functions

parse_constraint_with_kvars

Type Aliases

Assignments

Type alias for qualifier assignments used in constraint solving