András Salamon (Oct 26 2026 at 01:52): András Salamon (Oct 26 2026 at 01:52):Is there a standard oracle-free way to apply a theorem stated for any enum type at a size that is computed inside the proof? My current approach uses Types_To_Sets which I would prefer to avoid.
(Also, as far as I can tell, cancel_type_definition's record hides oracles from thm_oracles.)
András Salamon (Oct 26 2026 at 02:07):I think this might boil down to: what are approved ways to simulate dependent types? Pointers to text would be welcome.
Alex Mobius (Oct 26 2026 at 15:34):I think it's either types-to-sets or writing some ML (which can use normal theorem constructors, no oracles needed). If you're fine with restating the fact for each type, I got good mileage out of custom Eisbach method for cookie cutting proofs.
András Salamon (Oct 27 2026 at 02:02):Thank you. Having now read more of the literature, the types-to-sets approach seems more idiomatic than I thought, and we might just stay with that.
Last updated: Nov 08 2026 at 20:15 UTC