Crate mikino_api

A minimal (1-)induction library.

Re-exports

pub extern crate rsmt2;

Modules

check

Types and helpers to check a transition system.

err

Error-handling.

expr

Defines the expression structure used to represent predicates.

parse

Backend parser (SMT-LIB) and frontend parser (requires the parser feature).

prelude

Common imports throughout this project.

trans

Transition system structures and helpers.

Macros

build_decls

Builds some declarations.

build_expr

Convenience macro, provides a DSL for writing expressions.

build_trans

Builds a transition system.

build_trans_expr

Builds an expression.

build_typ

Builds a type.

prelude

Imports mikino’s prelude.

Constants

DEMO

String representation of a simple demo system, requires the demo feature.