9 lines
141 B
Text
9 lines
141 B
Text
|
import logic data.unit
|
||
|
|
|
||
|
|
structure point (A : Type) (B : Type) :=
|
||
|
|
mk :: (x : A) (y : B)
|
||
|
|
|
||
|
|
open point
|
||
|
|
|
||
|
|
check rec -- error, rec is protected
|