|
Construct `finfun_of` directly from a bespoke indexed inductive type,
which both makes it structurally positive (and therefore usable as a
container in an `Inductive` definition), and accommodates naturally
dependent functions.
This is still WIP, because this PR exposed a serious shortcoming of
the Coq unification algorithm’s implantation of Miller patterns. This
bug defeats the inference of `Canonical` structures for `{ffun S -> T}`
when the instances are defined in the dependent case!
This causes unmanageable regressions starting in `matrix.v`, so I
have not been able to check for any impact past that. I’m pushing this
commit so that the Coq issue may be addressed.
Made `fun_of_fin` structurally decreasing: Changed the primitive
accessor of `finfun_of` from `tfgraph` to the `Funclass` coercion
`fun_of_fin`. This will make it possible to define recursive functions
on inductive types built using finite functions. While`tfgraph` is
still useful to transport the tuple canonical structures to
`finfun_of`, it is no longer central to the theory so its role has
been reduced.
|
