open IO (Error) in

Stream: new members

[kaminsod]

Hi, can someone help me understand the meaning of this code (from lean4 codebase)?

open IO (Error) in
abbrev IO : Type → Type := EIO Error

What is the meaning or 'open' .. 'in', and 'abbrev'?

[Julian Berman]

open Foo means "I want to type bar and be able to have that potentially mean Foo.bar"
open Foo (eggs) means "only do that for Foo.eggs, not Foo.spam"
open .. in means "restrict the above to just the next command, not the whole file"
abbrev is a way to create an abbreviation (an alias) for a type.
So all in all that line defines the IO type as an abbreviation of some other type.

[kaminsod]

thanks!