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 18 2021 at 23:14 UTC