Bolton Bailey
Bolton Bailey
Hello, checking in to report that this is still a problem as of May 2021.
Actually, after more experimentation, I'm not convinced I understand `repeat` yet.
> We already have (essentially) this definition, it's called `nat.partrec.code`. > > > Create a mapping from mu_recursive, which describes algorithms, to the functions those algorithms compute. > > This...
See discussion [here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Is.20.60to_partrec.2Ecode.60.20actually.20efficient.3F/near/276439783) this might not work.
@prakol16 Seeing as how you're using a different code definition I would suggest making a new PR or PRs. Feel free to reuse any of the code here if it's...
Actually, check that, the first one is ok, the rest are broken though.
#2240 appears potentially relevant.
For future reference, I was able to fix the `menhir` issue by installing it, and the `ocamlformat` issue by `opam update` followed by `opam upgrade`. Perhaps these should be added...
Just another thing I've found to try to convince people this issue is important: In a discussion on the zulip, someone brought up "big_operators" and I didn't know what it...
Here are [two](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Type.20mismatch.20.60Iff.2Erfl.60.20in.20instance.20defintion/near/435705015) [more](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Compiler.20IR.20check.20failed/near/435953320) examples from Zulip.