Stream: Beginner Questions

Topic: Shorthand syntax for constructors


view this post on Zulip 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?

view this post on Zulip 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: Mar 28 2024 at 16:17 UTC