Christian Zimmerer (Dec 16 2022 at 22:32): Christian Zimmerer (Dec 16 2022 at 22:32):Is there a more concise way to express
"interp_c (I d ic ir) (All r c) = (let int = (I d ic ir)
in <something that uses int as well as its inner values>"
? Can I somehow abbreviate the (I d ic ir) constructor without a let binding, like the Haskell xxs@(x:xs) syntax?
Simon Roßkopf (Dec 16 2022 at 23:20):There is HOL-Library.Pattern_Aliases. After importing it and unbundle pattern_aliases you can write something like (I d ic ir =: i). There are some more examples and explanation in the Pattern_Aliases theory. I have, however, never used this in "production", so I do not know how well this works.
Last updated: Nov 13 2025 at 04:27 UTC