9 lines
175 B
Text
9 lines
175 B
Text
example : ℕ → ℕ :=
|
||
begin
|
||
exact id
|
||
--^ "command": "info"
|
||
end
|
||
--^ "command": "info"
|
||
|
||
example : ℕ → ℕ := by exact id
|
||
--^ "command": "info"
|