Email Gateway (Aug 18 2022 at 13:13): Email Gateway (Aug 18 2022 at 13:13):From: Scott West <scott.west@inf.ethz.ch>
Hello all,
I was just wondering if anyone could provide some advice for the
following design goal: take an existing type and instantiate it to some
theory without endlessly wrapping/unwrapping things.
For example, I may create a type:
int_func :: int => int
Then I later want to instantiate it in some theory, I can't have such a
type synonym, so I wrap it in a datatype constructor. However, this
tends to mean that I have to reproduce all the conceptually simpler
proofs on "int => int" to "IntFunc"-wrapped version of it, duplicating
my proofs for seemingly no reason.
Is there a nice way to lift proofs automatically, or somehow avoid this
issue entirely? Thanks!
Regards,
Scott West
(Sorry for any duplication)
Last updated: May 03 2024 at 04:19 UTC