Zulip Chat Archive

Stream: lean4

Topic: build simp syntax?

Daniel Selsam (Apr 13 2021 at 17:24):

Anyone know a good way to go from a lemmas : Array Syntax to the syntax representing by simp [<lemmas>]?

Daniel Selsam (Apr 13 2021 at 17:26):

Do I need to manually simulate all the other stuff in https://github.com/leanprover/lean4/blob/master/src/Init/Notation.lean#L269 ?

Sebastian Ullrich (Apr 13 2021 at 17:27):

Untested:

`(by simp [$[$lemmas:term],*])

Last updated: May 02 2025 at 03:31 UTC