File tree Expand file tree Collapse file tree 1 file changed +12
-8
lines changed Expand file tree Collapse file tree 1 file changed +12
-8
lines changed Original file line number Diff line number Diff line change @@ -37,14 +37,18 @@ private lemma abs_in : ⟨1, absRat⟩ ∈ exampleFiniteValuedCSP := rfl
37
37
private def exampleFiniteValuedInstance : exampleFiniteValuedCSP.Instance (Fin 2 ) :=
38
38
{ValuedCSP.unaryTerm abs_in 0 , ValuedCSP.unaryTerm abs_in 1 }
39
39
40
- example : exampleFiniteValuedInstance.IsOptimumSolution ![(0 : ℚ), (0 : ℚ)] := by
41
- intro s
42
- convert_to 0 ≤ exampleFiniteValuedInstance.evalSolution s
43
- rw [ValuedCSP.Instance.evalSolution, exampleFiniteValuedInstance]
44
- convert_to 0 ≤ |s 0 | + |s 1 |
45
- · simp [ValuedCSP.unaryTerm, ValuedCSP.Term.evalSolution, Function.OfArity.uncurry]
46
- rfl
47
- positivity
40
+ #adaptation_note
41
+ /--
42
+ This example stopped working on nightly-2024-09-05.
43
+ -/
44
+ -- example : exampleFiniteValuedInstance.IsOptimumSolution ![(0 : ℚ), (0 : ℚ)] := by
45
+ -- intro s
46
+ -- convert_to 0 ≤ exampleFiniteValuedInstance.evalSolution s
47
+ -- rw [ValuedCSP.Instance.evalSolution, exampleFiniteValuedInstance]
48
+ -- convert_to 0 ≤ |s 0| + |s 1|
49
+ -- · simp [ValuedCSP.unaryTerm, ValuedCSP.Term.evalSolution, Function.OfArity.uncurry]
50
+ -- rfl
51
+ -- positivity
48
52
49
53
-- ## Example: B ≠ A ≠ C ≠ D ≠ B ≠ C with three available labels (i.e., 3-coloring of K₄⁻)
50
54
You can’t perform that action at this time.
0 commit comments