batteries
batteries copied to clipboard
leanprover-community
The "batteries included" extended library for the Lean programming language and theorem prover
when i run "traced_repo = trace(repo) "I met the error below: `Traceback (most recent call last): File "/data1/yanhuiyuan/workspace/InternLM-Math/tests/test_lean_dojo.py", line 12, in traced_repo = trace(repo) ^^^^^^^^^^^ File "/home/yanhuiyuan/anaconda3/envs/atp/lib/python3.11/site-packages/lean_dojo/data_extraction/trace.py", line 250, in...
New attempt at well founded streams. Note that the old `Batteries.Data.Stream` file was moved *verbatim* to `Batteries.Data.Stream.Basic` and now `Batteries.Data.Stream` is just an import file. These facts don't show well...
Basic polynomial operations over the two-element field GF(2) using `BitVec`. Very basic for now. We will need to think about a friendly API and integration with Mathlib in the near...
This PR adds definitions for several `Float` functions (through axioms) and proves several theorems about `Float`. This is currently a WIP experiment.
In only one case a `Core.Context` is created from within CoreM, and we inherit from the parent Context the `initHeartbeats`. Otherwise, we get the current heartbeats from IO. It's not...
`alias` correctly handles `noncomputable` on a `def`, but not `noncomputable` on a `section`: ``` import Batteries.Tactic.Alias noncomputable def foo : Nat := Classical.choice sorry alias bar := foo -- works...
Metadata
Owner
Metadata
The "batteries included" extended library for the Lean programming language and theorem prover