From 9365082d98d7c1b95c40a9dafafc5a29bdc03ae9 Mon Sep 17 00:00:00 2001 From: Your Date: Sun, 4 Oct 2026 20:35:58 +0200 Subject: [PATCH] fix: port to Lean v4.33.1 (toolchain, manifest, tactic adaptations) - lean-toolchain + lake-manifest.json: v4.31.0 -> v4.33.1, same pins as consumer formal_logic_lean (mathlib 0df444a3, Foundation 81810b9f, batteries 4488d40d) - AdjunctiveSet: explicit Subset field value (v4.33 rejects the self-referential synthesized instance) - Logic/Semantics:219: explicit application in the reverse iff direction - Modal/LogicSymbol:347,430: dsimp -> simp (dsimp no longer fires closing simp lemmas) - Neighborhood/Semantics/Completeness:264: term-mode .trans proof (rw/unfold fragile on abbrev+lambda under implicit transparency) - Neighborhood/Semantics/Filtration: open Finset membership by lemma application (Finset.mem_filter) instead of rcases whnf - Neighborhood/Semantics/AxiomN: direct ContainsUnit instance on the abbrev head (v4.33 instance search no longer unfolds intermediateRelativeMaximalCanonicalModel to match the general relativeBasicCanonicalModel instance) lake build: SUCCESS (1230 jobs) under v4.33.1 lake build ModalLogicArchive.Modal.Kripke.Logic.S5: SUCCESS (1081 jobs) Co-Authored-By: Claude Haiku 4.5 (1M context) --- ModalLogicArchive/Logic/Semantics.lean | 3 +- ModalLogicArchive/Modal/LogicSymbol.lean | 4 +- ModalLogicArchive/Vorspiel/AdjunctiveSet.lean | 2 + Neighborhood/Semantics/AxiomN.lean | 10 + Neighborhood/Semantics/Completeness.lean | 10 +- Neighborhood/Semantics/Filtration.lean | 30 +- lake-manifest.json | 403 ++++++++++-------- lean-toolchain | 2 +- 8 files changed, 282 insertions(+), 182 deletions(-) diff --git a/ModalLogicArchive/Logic/Semantics.lean b/ModalLogicArchive/Logic/Semantics.lean index a9b4e4a..bba701b 100644 --- a/ModalLogicArchive/Logic/Semantics.lean +++ b/ModalLogicArchive/Logic/Semantics.lean @@ -216,7 +216,8 @@ instance empty' (𝓜 : M) : 𝓜 ⊧* (∅ : Set F) := ⟨by simp⟩ 𝓜 ⊧* Set.range φ ↔ ∀ i, 𝓜 ⊧ φ i := by simp [modelsSet_iff] @[simp] lemma setOf_iff {P : F → Prop} {𝓜 : M} : - 𝓜 ⊧* setOf P ↔ ∀ φ, P φ → 𝓜 ⊧ φ := by simp [modelsSet_iff] + 𝓜 ⊧* setOf P ↔ ∀ φ, P φ → 𝓜 ⊧ φ := by + rw [modelsSet_iff]; exact ⟨fun h φ hP => h hP, fun h φ hP => h φ hP⟩ end ModelsSet diff --git a/ModalLogicArchive/Modal/LogicSymbol.lean b/ModalLogicArchive/Modal/LogicSymbol.lean index 1fdce23..d00cd08 100644 --- a/ModalLogicArchive/Modal/LogicSymbol.lean +++ b/ModalLogicArchive/Modal/LogicSymbol.lean @@ -344,7 +344,7 @@ prefix:90 "□'" => List.LO.box @[simp, grind =] lemma boxItr_nil : (□^[n]'([] : List F)) = [] := by rfl -@[simp, grind =] lemma boxItr_single : (□^[n]'[φ]) = [□^[n]φ] := by dsimp [boxItr]; +@[simp, grind =] lemma boxItr_single : (□^[n]'[φ]) = [□^[n]φ] := by simp [boxItr]; @[simp, grind =] lemma eq_boxItr_conn : (□^[n]'(ψ :: s)) = (□^[n]ψ) :: (□^[n]'s) := by induction s <;> simp_all [boxItr]; @[simp, grind =] lemma eq_box_conn : (□' (ψ :: s)) = (□ψ) :: □'s := eq_boxItr_conn (n := 1) @@ -427,7 +427,7 @@ prefix:90 "◇'⁻¹" => List.LO.predia @[simp, grind =] lemma diaItr_nil : (◇^[n]'([] : List F)) = [] := by rfl @[simp, grind =] lemma prediaItr_nil : (◇⁻¹^[n]'([] : List F)) = [] := by rfl -@[simp, grind =] lemma diaItr_single : (◇^[n]'[φ]) = [◇^[n]φ] := by dsimp [diaItr]; +@[simp, grind =] lemma diaItr_single : (◇^[n]'[φ]) = [◇^[n]φ] := by simp [diaItr]; @[simp, grind =] lemma eq_diaItr_conn : (◇^[n]'(ψ :: s)) = (◇^[n]ψ) :: (◇^[n]'s) := by induction s <;> simp_all [diaItr]; @[simp, grind =] lemma eq_dia_conn : (◇' (ψ :: s)) = (◇ψ) :: ◇'s := eq_diaItr_conn (n := 1) diff --git a/ModalLogicArchive/Vorspiel/AdjunctiveSet.lean b/ModalLogicArchive/Vorspiel/AdjunctiveSet.lean index f06af50..a08184a 100644 --- a/ModalLogicArchive/Vorspiel/AdjunctiveSet.lean +++ b/ModalLogicArchive/Vorspiel/AdjunctiveSet.lean @@ -24,6 +24,7 @@ class AdjunctiveSet (β : outParam Type*) (α : Type*) extends Membership β α, attribute [simp] AdjunctiveSet.not_mem_empty AdjunctiveSet.mem_cons_iff instance Set.adjunctiveSet : AdjunctiveSet α (Set α) where + toHasSubset := ⟨fun s t => ∀ ⦃a⦄, a ∈ s → a ∈ t⟩ subset_iff := iff_of_eq Set.subset_def not_mem_empty := by simp mem_cons_iff := by simp [Adjoin.adjoin] @@ -39,6 +40,7 @@ instance Multiset.adjunctiveSet : AdjunctiveSet α (Multiset α) where mem_cons_iff := by simp [Adjoin.adjoin] instance Finset.adjunctiveSet [DecidableEq α] : AdjunctiveSet α (Finset α) where + toHasSubset := ⟨fun s t => ∀ ⦃a⦄, a ∈ s → a ∈ t⟩ subset_iff := Finset.subset_iff not_mem_empty := by simp mem_cons_iff := by simp [Adjoin.adjoin] diff --git a/Neighborhood/Semantics/AxiomN.lean b/Neighborhood/Semantics/AxiomN.lean index b52ec38..dd88d0a 100644 --- a/Neighborhood/Semantics/AxiomN.lean +++ b/Neighborhood/Semantics/AxiomN.lean @@ -52,6 +52,16 @@ instance {P : MaximalConsistentSet L → Set (Proofset L)} [L.HasAxiomN] : apply iff_of_true _ (Set.mem_univ Ω) exact Or.inl ⟨⊤, MaximalConsistentSet.mem_of_prove (by simp), by simp⟩ +/-- Direct instance on the abbrev head: under Lean v4.33, instance search no longer unfolds +`intermediateRelativeMaximalCanonicalModel` (an abbrev of `relativeBasicCanonicalModel`) to match +the general instance above. -/ +instance [L.HasAxiomN] : + (intermediateRelativeMaximalCanonicalModel L).ContainsUnit := by + constructor + ext Ω + apply iff_of_true _ (Set.mem_univ Ω) + exact Or.inl ⟨⊤, MaximalConsistentSet.mem_of_prove (by simp), by simp⟩ + end end diff --git a/Neighborhood/Semantics/Completeness.lean b/Neighborhood/Semantics/Completeness.lean index 61eeccf..d805d57 100644 --- a/Neighborhood/Semantics/Completeness.lean +++ b/Neighborhood/Semantics/Completeness.lean @@ -260,13 +260,9 @@ abbrev minimalRelativeMaximalCanonicalModel (L : Logic α) [L.Cl] [L.HasRE] [Non relativeBasicCanonicalModel L (fun _ _ => False) lemma minimalRelativeMaximalCanonicalModel.iff_minimal : - Ω ∈ (minimalRelativeMaximalCanonicalModel L).box X ↔ Ω ∈ (basicCanonicalModel L).box X := by - rw [relativeBasicCanonicalModel.iff_mem_box] - constructor - · rintro (h | ⟨_, h⟩) - · exact h - · exact h.elim - · exact Or.inl + Ω ∈ (minimalRelativeMaximalCanonicalModel L).box X ↔ Ω ∈ (basicCanonicalModel L).box X := + (relativeBasicCanonicalModel.iff_mem_box (P := fun _ _ => False)).trans + ⟨fun h => h.elim id (fun ⟨_, h'⟩ => h'.elim), fun h => Or.inl h⟩ /-- `relativeBasicCanonicalModel` with every non-proofset as an extra neighborhood. -/ abbrev maximalRelativeMaximalCanonicalModel (L : Logic α) [L.Cl] [L.HasRE] [Nonempty (MaximalConsistentSet L)] : diff --git a/Neighborhood/Semantics/Filtration.lean b/Neighborhood/Semantics/Filtration.lean index 5a09a6d..2ad31d9 100644 --- a/Neighborhood/Semantics/Filtration.lean +++ b/Neighborhood/Semantics/Filtration.lean @@ -385,7 +385,9 @@ lemma iff_mem_B : apply minimalFiltration.iff_mem_B.mpr; use φ; . right; - suffices (∃ Y, 【M (□φ)】 = (minimalFiltration M T).B Y) ∧ W ∈ 【M (□φ)】 by simpa; + suffices (∃ Y, 【M (□φ)】 = (minimalFiltration M T).B Y) ∧ W ∈ 【M (□φ)】 by + rw [if_pos this.1]; + exact this.2; constructor; . use (【M.truthset φ】); rw [Filtration.box_in_out hφ] @@ -575,7 +577,12 @@ def quasiFilteringTransitiveFiltration (M : Model κ α) [M.IsMonotonic] [M.IsTr (∀ ξ, □ξ ∈ T → 【M (□ξ)】 ∈ Ys → W ∈ 【M (□ξ)】 → A ∈ 【M (□ξ)】) ↔ (∀ ξ, □ξ ∈ T → ∀ Yi ∈ Ys, Yi = 【M (□ξ)】 → W ∈ 【M (□ξ)】 → A ∈ Yi) by simp [Ξ, Us]; - tauto; + constructor; + . rintro h i hi; + rcases Finset.mem_filter.mp hi with ⟨hiYs, ψ, hψ, rfl, hW⟩; + exact h ψ hψ hiYs hW; + . rintro h a ha hYs hW; + exact h _ (Finset.mem_filter.mpr ⟨hYs, a, ha, rfl, hW⟩); constructor; . rintro h _ _ _ _ rfl; apply h <;> assumption; @@ -588,7 +595,12 @@ def quasiFilteringTransitiveFiltration (M : Model κ α) [M.IsMonotonic] [M.IsTr (∀ ψ, □ψ ∈ T → 【M ψ】 ∈ Ys → W ∈ 【M (□ψ)】 → A ∈ 【M ψ】) ↔ (∀ ψ, □ψ ∈ T → ∀ Yi ∈ Ys, Yi = 【M ψ】 → W ∈ 【M (□ψ)】 → A ∈ Yi) by simp [Ψ, Vs]; - tauto; + constructor; + . rintro h i hi; + rcases Finset.mem_filter.mp hi with ⟨hiYs, ψ, hψ, rfl, hW⟩; + exact h ψ hψ hiYs hW; + . rintro h a ha hYs hW; + exact h _ (Finset.mem_filter.mpr ⟨hYs, a, ha, rfl, hW⟩); constructor; . rintro h _ _ _ _ rfl; apply h <;> assumption; @@ -692,10 +704,18 @@ def quasiFilteringTransitiveFiltration (M : Model κ α) [M.IsMonotonic] [M.IsTr rw [eYVU, this.1, this.2]; exact Finset.union_empty _; constructor; - . suffices ∀ Yi ∈ Ys, ∀ ψ, □ψ ∈ T → Yi = 【M ψ】 → ⟦w⟧ ∉ 【M (□ψ)】 by simpa [Vs]; + . suffices ∀ Yi ∈ Ys, ∀ ψ, □ψ ∈ T → Yi = 【M ψ】 → ⟦w⟧ ∉ 【M (□ψ)】 by + simp only [Vs, Finset.eq_empty_iff_forall_notMem]; + rintro Yi hi; + rcases Finset.mem_filter.mp hi with ⟨hYi, ψ, hψ, rfl, hw⟩; + exact this _ hYi ψ hψ rfl hw; rintro Yi hYi ψ hψ rfl hw; exact hΨ ⟨⟨ψ, hψ, ⟨_, hYi, rfl⟩, hw⟩⟩; - . suffices ∀ Yi ∈ Ys, ∀ ξ, □ξ ∈ T → Yi = 【M (□ξ)】 → ⟦w⟧ ∉ 【M (□ξ)】 by simpa [Us]; + . suffices ∀ Yi ∈ Ys, ∀ ξ, □ξ ∈ T → Yi = 【M (□ξ)】 → ⟦w⟧ ∉ 【M (□ξ)】 by + simp only [Us, Finset.eq_empty_iff_forall_notMem]; + rintro Yi hi; + rcases Finset.mem_filter.mp hi with ⟨hYi, ξ, hξ, rfl, hw⟩; + exact this _ hYi ξ hξ rfl hw; rintro Yi hYi ξ hξ rfl hw; exact hΞ ⟨⟨ξ, hξ, ⟨_, hYi, rfl⟩, hw⟩⟩; . intro h; diff --git a/lake-manifest.json b/lake-manifest.json index d1fe94e..404e642 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,166 +1,237 @@ -{"version": "1.2.0", - "packagesDir": ".lake/packages", - "packages": - [{"url": "https://github.com/SnO2WMaN/lean-typst.git", - "type": "git", - "subDir": null, - "scope": "", - "rev": "2158f3dec8911bc8cb1afc7fd1bc95b0e58d42fb", - "name": "LeanTypst", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": false, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/FormalizedFormalLogic/Foundation", - "type": "git", - "subDir": null, - "scope": "", - "rev": "b62b3bac1bbd44ca8a7f7159340a0b0193d12b3e", - "name": "Foundation", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": false, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/ProofWidgets4", - "type": "git", - "subDir": null, - "scope": "", - "rev": "24b0d9dc081c5423f8eec7e866c441e5184f29d9", - "name": "proofwidgets", - "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.102", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/mathlib4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "fabf563a7c95a166b8d7b6efca11c8b4dc9d911f", - "name": "mathlib", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/doc-gen4", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "0bc516c1b9db83658d6475c40d9b1ed71219b921", - "name": "«doc-gen4»", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover-community/plausible", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "63045536fe95024e6c18fc7b48e03f506701c5bc", - "name": "plausible", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/LeanSearchClient", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "c5d5b8fe6e5158def25cd28eb94e4141ad97c843", - "name": "LeanSearchClient", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/import-graph", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "5c7542ed018c78194f1e2b903eaf6a792b74c03d", - "name": "importGraph", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/aesop", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "e3cb2f741431ce31bf73549fb52316a57368b06f", - "name": "aesop", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/quote4", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "f46324995fca5f0483b742e4eb4daec7f4ee50d2", - "name": "Qq", - "manifestFile": "lake-manifest.json", - "inputRev": "master", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover-community/batteries", - "type": "git", - "subDir": null, - "scope": "leanprover-community", - "rev": "fa08db58b30eb033edcdab331bba000827f9f785", - "name": "batteries", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/leanprover/leansqlite", - "type": "git", - "subDir": null, - "scope": "", - "rev": "0be4df908d1a8e75b58961041e2b4973692623df", - "name": "leansqlite", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/leanprover/lean4-cli", - "type": "git", - "subDir": null, - "scope": "leanprover", - "rev": "92564e5770e4d09f2d86dfbf8ada1e9c715b384c", - "name": "Cli", - "manifestFile": "lake-manifest.json", - "inputRev": "v4.31.0", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/fgdorais/lean4-unicode-basic", - "type": "git", - "subDir": null, - "scope": "", - "rev": "a2e430a4c9d3ad24078b8581fe0162fc5b0c9a6c", - "name": "UnicodeBasic", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}, - {"url": "https://github.com/dupuisf/BibtexQuery", - "type": "git", - "subDir": null, - "scope": "", - "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", - "name": "BibtexQuery", - "manifestFile": "lake-manifest.json", - "inputRev": "nightly-testing", - "inherited": true, - "configFile": "lakefile.toml"}, - {"url": "https://github.com/acmepjz/md4lean", - "type": "git", - "subDir": null, - "scope": "", - "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", - "name": "MD4Lean", - "manifestFile": "lake-manifest.json", - "inputRev": "main", - "inherited": true, - "configFile": "lakefile.lean"}], - "name": "ProvabilityLogic", - "lakeDir": ".lake", - "fixedToolchain": false} +{ + "version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [ + { + "url": "https://github.com/SnO2WMaN/lean-typst.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "2158f3dec8911bc8cb1afc7fd1bc95b0e58d42fb", + "name": "LeanTypst", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/FormalizedFormalLogic/Foundation.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "81810b9f22c49fbb32bd89c1e9737059d83a37e6", + "name": "Foundation", + "manifestFile": "lake-manifest.json", + "inputRev": "81810b9f22c49fbb32bd89c1e9737059d83a37e6", + "inherited": false, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/mathlib4.git", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "0df444a360eaa60ab8c11dca51a86af692955474", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.1", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover/doc-gen4", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "0bc516c1b9db83658d6475c40d9b1ed71219b921", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.31.0", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/leanprover/leansqlite", + "type": "git", + "subDir": null, + "scope": "", + "rev": "0be4df908d1a8e75b58961041e2b4973692623df", + "name": "leansqlite", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/leanprover/lean4-cli", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.33.0", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "a2e430a4c9d3ad24078b8581fe0162fc5b0c9a6c", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "5d31b64fb703c5d77f6ef4d1fb958f9bdf1ea539", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "nightly-testing", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "6a3fb240133bcb7e1a066fdc784b3fdc304e3fc5", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean" + }, + { + "url": "https://github.com/FormalizedFormalLogic/ProvabilityLogic.git", + "type": "git", + "subDir": null, + "scope": "", + "rev": "01628c51f618fd11f2f6b10c813f261f1d36c7a6", + "name": "ProvabilityLogic", + "manifestFile": "lake-manifest.json", + "inputRev": "01628c51f618fd11f2f6b10c813f261f1d36c7a6", + "inherited": false, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/FormalizedFormalLogic/forgive", + "type": "git", + "subDir": null, + "scope": "", + "rev": "32667a1902df73e5f27cdfcef57855e6b8b24d55", + "name": "Forgive", + "manifestFile": "lake-manifest.json", + "inputRev": "32667a1902df73e5f27cdfcef57855e6b8b24d55", + "inherited": true, + "configFile": "lakefile.toml" + }, + { + "url": "https://github.com/SnO2WMaN/axiom-audit", + "type": "git", + "subDir": null, + "scope": "", + "rev": "827e715d39231df230cb5b1a200be07c151b323b", + "name": "«axiom-audit»", + "manifestFile": "lake-manifest.json", + "inputRev": "827e715d39231df230cb5b1a200be07c151b323b", + "inherited": true, + "configFile": "lakefile.toml" + } + ], + "name": "ProvabilityLogic", + "lakeDir": ".lake", + "fixedToolchain": false +} \ No newline at end of file diff --git a/lean-toolchain b/lean-toolchain index 133a3f7..a8afa7d 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.31.0 \ No newline at end of file +leanprover/lean4:v4.33.1