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