5 lines
78 B
Text
5 lines
78 B
Text
|
definition foo (x : empty) : empty :=
|
||
|
|
by try exact _;contradiction
|
||
|
|
|
||
|
|
print foo
|