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