lean4
lean4 copied to clipboard
leanprover
Lean 4 programming language and theorem prover
I pulled `intMin` and `intMax` up in the `Lemmas` file. To do so, I had to move other sections down. Most significant changes include: 1. moving `toNat_shiftLeft` and `getLsbD_shiftLeft` out...
### Description ``` import Std.Data.BitVec.Basic import Std.Data.Bitvec.Basic -- ``Bitvec`` should have been ``BitVec`` ``` Fails with ``` import Std.Data.Bitvec.Basic failed, environment already contains 'Std.BitVec.smod._cstage1' from Std.Data.BitVec.Basic ``` while it should...
### Proposal Right now, we have `IO : Type → Type`. This RFC suggests we change to `IO : Type u → Type u`. This RFC does *not* suggest: *...
Making this issue per discussion [here](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/lake.20errors/near/409315479). I was trying to install Duper and got the following error which confused me: ``` boltonbailey@starlight drafting % lake update duper warning: drafting: package...
### The issue A user might expect to be able to write this function, and be able to proof it terminating (or even have the default `decreasing_tactic` prove it terminating):...
### Prerequisites * [X ] Put an X between the brackets on this line if you have done all of the following: * Check that your issue is not already...
### Prerequisites * [X] Put an X between the brackets on this line if you have done all of the following: * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues)....
### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues)....
### Prerequisites * [x] Put an X between the brackets on this line if you have done all of the following: * Check that your issue is not already [filed](https://github.com/leanprover/lean4/issues)....
Metadata
Owner
Metadata
Lean 4 programming language and theorem prover