Markus Himmel comments

Results 16 comments of


                                            Markus Himmel

feat: Std.HashMap

@david-christiansen Thank you very much for the detailed review! I'll give you a chance to confirm that all of your comments have been addressed and then I think it's time...

"Try this" suggestion includes trailing comments

Jujian Zhang just ran into this while demoing Lean to a bunch of people in Durham :)

`Rat` normalization should use an `@[extern]` backed by `mpz_divexact`

Where did this issue come from? Is there reason to believe that `Rat` normalization is the bottleneck somewhere?

`interval_cases` for `pnat`s does not work, because `norm_num` does not support `pnat` (except sometimes)

> Could you clarify this issue so it actually says what fails? I have updated the issue text with the error messages. I haven't tracked down why `norm_num` fails to...

feat: expand logic to determine local time

Thanks for the PR! > I would kindly ask for help with writing a test for the `TZ` environment variable since I am very new to lean. More specifically: How...

feat: expand logic to determine local time

> Is there anything blocking this MR? Just a lack of review capacity :)