swh:1:snp:ca722f838562be139d7880d2b37d9db111694bf0
Revision 66c830f9593684da87d07c365a68f1a17156de74 authored by François Dupressoir on 15 June 2020, 14:55:33 UTC, committed by François Dupressoir on 15 June 2020, 14:55:33 UTC
Now reduced to PROM as core, with ROM as a simpler interface.

PROM is concrete to allow reuse of its flag type.
Its internal theories, and ROM, are abstract to avoid growing forests of clones
when using eager arguments.

ROM now aligns with PROM in cloning interface: additional types `d_in_t` and `d_out_t`
specify the distinguisher's interface. (This simplifies instantiation.)

Some changes to type and oracle names to make them more explicit. Notably:
- `from` is now `in_t`,
- `to` is now `out_t`, (with associated change on name of distribution).
1 parent 734e5bb
History
Tip revision: 701f4f03c094eb2441f511fed1df042080fdf34e authored by Cameron Low on 20 January 2023, 18:18:02 UTC
Unify created variables correctly.
Tip revision: 701f4f0
File Mode Size
config
examples
lint
scripts
src
theories
.dir-locals.el -rw-r--r-- 285 bytes
.gitignore -rw-r--r-- 515 bytes
.merlin -rw-r--r-- 241 bytes
.travis.yml -rw-r--r-- 2.7 KB
COPYRIGHT -rw-r--r-- 581 bytes
COPYRIGHT.yaml -rw-r--r-- 596 bytes
MANIFEST -rw-r--r-- 596 bytes
Makefile -rw-r--r-- 4.8 KB
Makefile.system -rw-r--r-- 555 bytes
README.md -rw-r--r-- 8.3 KB
_tags -rw-r--r-- 812 bytes
default.nix -rw-r--r-- 305 bytes
myocamlbuild.ml -rw-r--r-- 2.3 KB

README.md

back to top