io

Stream: general

[Reid Barton]

Is it intentional that the whole io interface (notably including various constants like monad_io_terminal) is not meta?

[Reid Barton]

I just wonder because for soundness, one ought to check that all these constants can be implemented (e.g., by io_core = lam x y, unit) in Lean

[Johannes Hölzl]

Yes, to ensure soundness we would need to show that it fulfills all constraints. But then all these classes are just lists of operations which do not contain any proposition. Showing that they are inhabited is trivial.

[Johannes Hölzl]

But a nice model would be cool, i.e. where io_core encapsulates a state with files, processes etc.

[Reid Barton]

I just wonder whether there's a reason that it is handled differently from tactic, where as far as I can tell all the constants are marked meta. Maybe it's just that tactic has quite a lot more constants, and also the definition of the tactic monad is partially exposed (as state something).

[Reid Barton]

The most interesting thing with io I found is that monad_io_terminal.cmdline_args io_core is a list string which is not meta, so I could do things like make a mathematical definition which depends on the length of this list

[Reid Barton]

Although #print axioms would reveal what I had done