package universo

You can search for identifiers within the package.

in-package search v0.2.0

A tool for Dedukti to play with universes

Install

Dune Dependency

github.com Readme Changelog Edit opam file Versions (1)

Authors

D

dedukti-dev@inria.fr

Maintainers

D

dedukti-dev@inria.fr

Sources

v2.7.tar.gz

sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c

sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

doc/universo.solving/Solving/Z3arith/Make/index.html

Module `Z3arith.Make`Source

Parameters

module Spec : L.LRA_SPECIFICATION

Signature

Sourcetype t = Z3.Expr.expr

Sourcetype smt_model = Z3.Model.model

Sourcetype ctx = Z3.context

Sourceval logic : [> `Lra ]

Sourceval mk_name : B.name -> string

Sourceval int_sort : Z3.context -> Z3.Sort.sort

Sourceval mk_var : ctx -> string -> t

Sourceval to_int : ctx -> int -> t

Sourceval mk_univ : ctx -> U.univ -> t

Sourceval mk_max : ctx -> t -> t -> t

Sourceval mk_imax : ctx -> t -> t -> t

Sourceval mk : (ctx, t) L.k

Sourceval mk_axiom : ctx -> t -> t -> t

Sourceval mk_rule : ctx -> t -> t -> t -> t

Sourceval mk_cumul : ctx -> t -> t -> t

Sourceval mk_bounds : ctx -> string -> int -> Z3.Expr.expr

Sourceval solution_of_var : ctx -> int -> Z3.Model.model -> string -> U.univ

Sourceval mk_theory : bool

On This Page

Parameters
Signature