diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean index 8796b5741f..64096c3609 100644 --- a/library/init/datatypes.lean +++ b/library/init/datatypes.lean @@ -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}