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: Dec 20 2023 at 11:08 UTC