Skip to content
Snippets Groups Projects
Forked from Iris / Iris
Source project has a limited visibility.
Isaac van Bakel's avatar
Isaac van Bakel authored
Previously, each individual instance in the option OFE and camera
instances (i.e. `Dist`, `Valid`, etc.) required a full OFE (resp.
camera) instance for the argument type of the option. This makes using
option in the definition of recursively-defined OFEs and cameras
annoyingly hard, since you can't use e.g. the option `Dist` to define
your recursive `Dist` instance, since your type isn't yet an OFE.

This change strengthens all these instances to just require an instance
of the same class on the argument type, so that they can be relied on for
implementing an OFE. Ideally all the lemmas associated with these
instances would also be strengthened, but these are harder to
generalise, so I've opted to skip over that work for now.
029c1857
History
Name Last commit Last update