Andrés Goens

feat: blocking behavior on EOF for readLine

1

As discussed in [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60lean.20--stdin.60.20does.20not.20respect.20Ctrl.2BD/near/292550058), this implements the blocking behavior seen by Rust. When a stream sees an EOF on a readLine, it will return an empty string once. When called...

Not-irrelevant proofs?

1

In `EffectKind.lean` we have a bunch of lemmata that take proofs of known theorems as statements, e.g. ```lean @[simp] theorem liftEffect_pure_impure [Monad m] (hle : pure ≤ impure) : liftEffect...

Because of dependently-typed shenanigans, the executable semantics only work for concrete tests (with no mvars in the bitwidth). We should fix this.