Alex Mobius (Mar 20 2026 at 18:56): Alex Mobius (Mar 20 2026 at 18:56):I have a datatype that's "'a fset \<times> (('a \<times> 'b) fset \<times> 'c) set" plus a condition that the left fset binds the domains of domain of the right set. This is a BNF in 'a, and I want to prove it. However, relators prove to be really annoying, auxiliary theorems for "rel_fset (rel_prod R (=))" alone already took me several pages, and normally BNF machinery can derive it all by itself. The rub here is that a set is not a BNF, but its relator obeys all the same rules, it is THE natural relator one could say :) so, is there a way to partially automate this derivation, in the fashion that BNF machinery does it, ideally without writing ML?
Jan van Brügge (Mar 23 2026 at 14:37):this type is not a BNF in 'a because it appears under the set type constructor? BNFs have to be bounded which set is not
Last updated: Apr 09 2026 at 09:11 UTC