Skip to content

Commit

Permalink
chore: drop unused dependency to lean4-partax (#313)
Browse files Browse the repository at this point in the history
  • Loading branch information
tobiasgrosser authored May 20, 2024
1 parent 889e8e8 commit 4062b06
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,5 @@ lean_lib AliveScaling {

require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
require Cli from git "https://github.com/mhuisi/lean4-cli.git" @ "nightly"
require partax from git "https://github.com/tydeu/lean4-partax" @ "master"
meta if get_config? doc = some "on" then -- dev is so not everyone has to build it
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

0 comments on commit 4062b06

Please sign in to comment.