search

opencompl / lean-mlir

A minimal development of SSA theory
Other
88 stars 10 forks source link

feat: doz, max and min theorems #555

Closed AnotherAlexHere closed 2 months ago

AnotherAlexHere commented 2 months ago

I added some new theorems on "difference or zero".

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

AtticusKuhn commented 2 months ago

Also, as a general comment, it seems that that HackersDelight.lean file is getting rather long, and this may slow down Lean in type-checking the file (because Lean type-checks files linearly from top to bottom). I would suggest splitting up HackersDelight.lean into several smaller files to increase modularity and hasten type-checking times.

tobiasgrosser commented 2 months ago

Also, as a general comment, it seems that that HackersDelight.lean file is getting rather long, and this may slow down Lean in type-checking the file (because Lean type-checks files linearly from top to bottom). I would suggest splitting up HackersDelight.lean into several smaller files to increase modularity and hasten type-checking times.

I think this is good to keep in mind. For now, I would prefer to keep things in a single file as this makes it easier to keep an overview of what exists.

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)

github-actions[bot] commented 2 months ago

Alive Statistics: 64 / 93 (29 failed)