Skip to content

Commit 4966ada

Browse files
jessealamaclaude
andcommitted
docs: add TODO comments for files that can't import Cslib.Init
Added commented-out import statements with explanations for two files that should ideally import Cslib.Init but cannot due to technical issues: - Cslib.Foundations.Data.FinFun: Notation conflict (→₀ used by both FinFun and Mathlib.Finsupp) - Cslib.Foundations.Semantics.LTS.Basic: Causes type elaboration ambiguities in downstream Automata files These comments document the issue and serve as reminders for future investigation. 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-Authored-By: Claude <[email protected]>
1 parent 34bc7dd commit 4966ada

File tree

2 files changed

+2
-0
lines changed

2 files changed

+2
-0
lines changed

Cslib/Foundations/Data/FinFun.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Fabrizio Montesi, Xueying Qin
55
-/
66

7+
-- import Cslib.Init -- TODO: Notation conflict with Mathlib.Finsupp (both use →₀)
78
import Mathlib.Data.Finset.Basic
89

910
/-! # Finite functions

Cslib/Foundations/Semantics/LTS/Basic.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Fabrizio Montesi
55
-/
66

7+
-- import Cslib.Init -- TODO: Causes type elaboration ambiguities in downstream files (Automata)
78
import Mathlib.Tactic.Lemma
89
import Mathlib.Data.Finite.Defs
910
import Mathlib.Data.Fintype.Basic

0 commit comments

Comments
 (0)