2015-05-26 18:33:38 +00:00
|
|
|
namespace foo
|
2016-01-27 02:24:12 +00:00
|
|
|
definition C₁ := nat
|
|
|
|
|
definition foo (c : C₁) := nat.rec_on c _ _
|
2015-05-26 18:33:38 +00:00
|
|
|
end foo
|
|
|
|
|
|
|
|
|
|
namespace boo
|
2016-01-27 02:24:12 +00:00
|
|
|
notation `C₁` := nat
|
|
|
|
|
definition foo (c : C₁) := nat.rec_on c _ _
|
2015-05-26 18:33:38 +00:00
|
|
|
end boo
|
