Skip to content

chore: address weekly linting report #1168

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
jessealama wants to merge 4 commits into
base: main
Choose a base branch
from
Open

chore: address weekly linting report #1168

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
4344ec3
chore(Circuit): prove a synthesis step directly instead of with grind
jessealama Oct 27, 2026
2a98f50
chore(CCS/VendingMachine): merge tactics into grind
jessealama Oct 27, 2026
9915512
doc(Query): close an inline code span in a docstring
jessealama Oct 27, 2026
20eda18
chore(Circuit): merge tactics into grind
jessealama Oct 28, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 1 addition & 2 deletions Cslib/Algorithms/CCS/VendingMachine.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,8 +84,7 @@ theorem vm_ltsD_ltsND_not_bisim : ¬(vm ~[ltsD, ltsND] vm) := by
let p₁ := `(CCS| (Tea. const Constant.vm) + (Coffee. const Constant.vm))
let q₁ := `(CCS| Tea. const Constant.vm)
have ltsD_vm_deterministic : ltsD.DeterministicStateLabel vm Coin := by
intro _ _ htr₁ htr₂
grind [const_tr htr₁, const_tr htr₂]
grind
have h : r p₁ q₁ :=
match_deterministic
hbisim hr
Expand Down
4 changes: 2 additions & 2 deletions Cslib/Algorithms/Lean/Query/Sort/LowerBound.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,8 +53,8 @@ private theorem finPrefix_injective (h : ↑n ≤ #α) :
(finEmbedding h).injective.extend_of_disjoint Sum.inl_injective Sum.inr_injective
Set.isCompl_range_inl_range_inr.disjoint

/-- A total order on an type `α` with at least `n` elements, that orders `n` embedded elements
(via `finEmbedding) according to `σ⁻¹`, with embedded elements
/-- A total order on a type `α` with at least `n` elements, that orders `n` embedded elements
(via `finEmbedding`) according to `σ⁻¹`, with embedded elements
preceding all others, and a well-ordering among non-embedded elements. -/
private noncomputable def PrefixPermOrder (h : ↑n ≤ #α)
(σ : Equiv.Perm (Fin n)) : α → α → Prop :=
Expand Down
3 changes: 1 addition & 2 deletions Cslib/Computability/Circuit/Full.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,8 +124,7 @@ private theorem exists_full_synthesis_finset [DecidableEq U]
obtain ⟨a, ha⟩ := exists_full_synthesis_point (f point) default point
obtain ⟨b, hb⟩ := ih
have hstep := ha.full_binary hb (fun v acc => if v = default then acc else v)
use a + b + 1
grind only [= Finset.mem_insert]
grind

private theorem fullInterpretation_isComplete_two [Finite U] :
(fullInterpretation (k := 2) (Carrier := U)).IsComplete where
Expand Down
Loading