lean2/tests/lean/notation5.lean

12 lines
118 B
Text
Raw Permalink Normal View History

import data.num
notation `((` := 1
precedence `(` : 30
notation `))` := 1
notation `,,` := 1
precedence `,` : 10