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

sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c

sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c

type t = Z3.Expr.expr

Type for formulas

type smt_model = Z3.Model.model

Model returns by the solver

type ctx = Z3.context

Meta informations needed by the solver

val logic : Utils.logic

Specify the logic implemented

val mk_name : Solving.Utils.B.name -> string

mk_name n returns a SMT string from a Dedukti name n

val mk_var : ctx -> string -> t

mk_var ctx s returns a variable expression as to the name s

val mk_univ : ctx -> Common.Universes.univ -> t

mk_univ ctx u returns an expression associated to the universe u

val mk_axiom : ctx -> t -> t -> t

mk_axiom ctx s s' returns an expression encoding the predicate A(s,s')

val mk_cumul : ctx -> t -> t -> t

mk_cumul ctx s s' returns an expression encoding the predicate C(s,s')

val mk_rule : ctx -> t -> t -> t -> t

mk_rule ctx s s' s'' returns an expression encoding the predicate R(s,s',s'')

val mk_bounds : ctx -> string -> int -> t

mk_bound ctx s i returns an expression encoding that a variable cannot be higher that the ith universe

val solution_of_var : 
  ctx ->
  int ->
  smt_model ->
  string ->
  Common.Universes.univ

solution_of_var ctx i model s returns the universe found by the SMT solver