10 lines
165 B
Text
10 lines
165 B
Text
|
namespace foo
|
||
|
|
open nat
|
||
|
|
inductive nat : Type := zero, foosucc : nat → nat
|
||
|
|
check 0 + nat.zero --error
|
||
|
|
end foo
|
||
|
|
|
||
|
|
namespace foo
|
||
|
|
check nat.succ nat.zero --error
|
||
|
|
end foo
|