2014-11-07 05:34:05 +00:00
|
|
|
import logic
|
|
|
|
|
|
|
|
|
|
constant f : num → num
|
|
|
|
|
constant g : num → num
|
|
|
|
|
notation a `+++` := f a
|
2015-10-14 01:35:16 +00:00
|
|
|
notation [parsing_only] a `***` := g a
|
2014-11-07 05:34:05 +00:00
|
|
|
check 10 +++
|
|
|
|
|
check 10 ***
|
|
|
|
|
check Type.{8} -- Type₊ should not be used
|
