max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library/init/datatypes): remove notation nobody uses

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-03 16:59:55 -07:00
parent 696b190a8d
commit 9a17d567ec
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/datatypes.lean
View file

@ -7,8 +7,6 @@ Basic datatypes
-/
prelude
notation `Prop` := Type.{0}
notation [parsing_only] `Type'` := Type.{_+1}
notation [parsing_only] `Type₊` := Type.{_+1}
notation `Type₁` := Type.{1}
notation `Type₂` := Type.{2}
notation `Type₃` := Type.{3}