4 lines
129 B
Text
4 lines
129 B
Text
set_option relaxedAutoImplicit false
|
|
instance has_arr : HasArr Preorder := { Arr := Function }
|
|
|
|
def foo : Nat := { first := 10 }
|