Matthew Robert Ballard

icon indicating a website link mattrobball.com

icon company University of South Carolina icon location Columbia, South Carolina, USA icon location I am a mathematician who sometimes fantasizes about being a physicist and/or computer scientist, depending on the day.

Results 61 comments of Matthew Robert Ballard

feat: Generalize corollaries of rank-nullity theorem.

Overall it is not terrible but it would nice to take a quick look at those two files to make sure you cannot make an easy change to fix the...

feat: Generalize corollaries of rank-nullity theorem.

After actually looking at the changes, this is perfectly fine.

rfc: allow universe unification to solve `max u v =?= max u ?v`

Can you summarize the reasoning for not doing this during typeclass synthesis?

rfc: allow universe unification to solve `max u v =?= max u ?v`

Breakage incoming: leanprover-community/mathlib4#12522 is waiting until I get back to a machine to figure out what is going on with the non-arm MacOS build. It builds with the custom toolchain....

Trace class `Meta.synthInstance.answer` is not registered

I have [branch](https://github.com/mattrobball/lean4/tree/newAnswer) which adds the trace messages in `addAnswer` to the `newAnswer` trace class. If this is favorable, let me know and I will PR.

Trace class `Meta.synthInstance.answer` is not registered

@thorimur had identified a more exhaustive list of such things

Configuration option for `synthPendingDepth`

Added references for failures in `OperatorNorm` in leanprover-community/mathlib4#12188

Configuration option for `synthPendingDepth`

It broke things pretty badly when I bumped the hardcoded bound from 0 to 1.

chore(Quiver.Opposite): make `Quiver.Hom.op/unop` `abbrev`'s

!bench

chore: remove unnecessary outParam

bors merge