Mario Carneiro

This is not a job for `norm_num`, which works from the inside out, evaluating terms to a normal form. What we need here is something like Isabelle's `approximation` tactic, but...

I don't think the article has any misconceptions about that, and the table is correct. But I also think that it is 8 years too late to be proposing something...

> > I don't think the article has any misconceptions about that, and the table is correct. But I also think that it is 8 years too late to be...

> @digama0 I meant that at that time Rust was irrelevant in a broader context (break changes weren't a problem like they are today) and influenced by few people, much...

A monad is a type constructor `M` with an operation `pure: fn(T) -> M`, `and_then: fn(M, fn(A) -> M) -> M` and some laws. Now `Fallible` is also a type...

Isn't it called [`unreachable_unchecked`](https://doc.rust-lang.org/std/hint/fn.unreachable_unchecked.html)? I notice you linked a docs page from 1.25 which is quite a while ago. (EDIT: actually I see you linked the name of the core...

Base conversion is algotihmically quadratic. (Every digit requires doing what amounts to `(n % 10, n / 10)` and there are not many shortcuts.) I don't think the List Char...

Yes, possibly, I'm just saying that these numbers don't demonstrate that. If large number literals are transitioned to use a `from_array` function instead of translating a string, the calls to...

Could you clarify this issue so it actually says what fails?

The problem is that `norm_num` needs `linear_ordered_semiring ℕ+` for the theorems it applies, but this is false. Either we need a better typeclass, or `norm_num` needs to special case `pnat`.