An error occurred while fetching folder content.
Forked from
Iris / Iris
Source project has a limited visibility.

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.
Name | Last commit | Last update |
---|