7 lines
No EOL
92 B
Text
7 lines
No EOL
92 B
Text
VISIT foo.lean
|
||
SYNC 3
|
||
import data.prod
|
||
open prod
|
||
definition foo A := λB, A × B
|
||
WAIT
|
||
INFO 3 |