Zulip Chat Archive

Stream: general

Topic: io


view this post on Zulip Reid Barton (Sep 15 2018 at 13:54):

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

view this post on Zulip Reid Barton (Sep 15 2018 at 13:56):

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

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 14:05):

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.

view this post on Zulip Johannes Hölzl (Sep 15 2018 at 14:07):

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

view this post on Zulip Reid Barton (Sep 15 2018 at 14:12):

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).

view this post on Zulip Reid Barton (Sep 15 2018 at 14:13):

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

view this post on Zulip Reid Barton (Sep 15 2018 at 14:16):

Although #print axioms would reveal what I had done


Last updated: May 11 2021 at 12:15 UTC