summaryrefslogtreecommitdiff
path: root/Nominal
ModeNameSize
-rw-r--r--Basic.lean21logplain