package universo
A tool for Dedukti to play with universes
Install
Dune Dependency
Authors
Maintainers
Sources
v2.7.tar.gz
sha512=97171b48dd96043d84587581d72edb442f63e7b5ac1695771aa1c3c9074739e15bc7d17678fedb7062acbf403a0bf323d97485c31b92376b80c63b5c2300ee3c
sha256=5e1b6a859dfa1eb2098947a99c7d11ee450f750d96da1720f4834e1505d1096c
doc/universo.solving/Solving/Solver/MakeUF/index.html
Module Solver.MakeUF
Source
Parameters
module S : Utils.SMTSOLVER
Signature
parse file
parses the constraint associated to file
print_model meta model file
prints the model into the solution file associated to file
. Universes are translated to terms via the meta
rules.
solve env
solves all the files parsed and returns a model as long as i
, the number of universes needed. As postconditions, i >= env.minimum && i <= maximum
. Moreover forall j < i
, the solver did not found a solution.
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page