Crate liquid_fixpoint 

This crate implements an interface to the liquid-fixpoint binary

Modules

constraint 🔒

format 🔒

parser

sexp

smt_horn

Macros

declare_types

Structs

Bind

ConstDecl

CrashInfo

DataCtor

DataDecl

DataField

Error

ErrorInner 🔒

FlatConstraint

FunBody

FunDef

FunSort

KVarBind

KVarDecl

QualParam

Qualifier

SortDecl

Stats

Task

VerificationResult

WKVar

Enums

BinOp

BinRel

Constant

Constraint

Expr

FixpointError

An error that prevented fixpoint from producing a result

FixpointStatus

LeanStatus

Pred

Quantifier

SmtSolver

Sort

SortCtor

ThyFunc

Traits

FixpointFmt

Identifier

Types

Type Aliases

Assignments

Type alias for qualifier assignments used in constraint solving