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):
`(by simp [$[$lemmas:term],*])
Last updated: May 18 2021 at 23:14 UTC