disabled tactics command #16

2023-02-06 14:59:41 +01:00
parent dd4fe60f7e
commit 51f82cf9eb
15 changed files with 41 additions and 20 deletions
@@ -28,3 +28,4 @@ HiddenHint : 42 = 42 =>
 Conclusion "Bravo! PS: `rfl` steht für \"reflexivity\"."

 NewTactics rfl
+DisabledTactics tauto
@@ -33,3 +33,4 @@ HiddenHint (n : ℕ) (h : 1 < n) : 1 < n =>
 Conclusion ""

 NewTactics assumption
+DisabledTactics tauto
@@ -28,3 +28,4 @@ HiddenHint (A : Prop) (hA : A) : A =>
 Conclusion ""

 NewTactics assumption
+DisabledTactics tauto
@@ -34,3 +34,4 @@ True := by
 Conclusion ""

 NewTactics trivial
+DisabledTactics tauto
@@ -22,3 +22,4 @@ Statement
 Conclusion ""

 NewTactics trivial
+DisabledTactics tauto
@@ -28,3 +28,4 @@ HiddenHint (A : Prop) (h : False) : A =>
 unabhängig davon, was das Goal ist."

 NewTactics contradiction
+DisabledTactics tauto
@@ -27,3 +27,4 @@ Conclusion
 "

 NewTactics contradiction
+DisabledTactics tauto
@@ -30,3 +30,4 @@ Conclusion
 "

 NewTactics contradiction
+DisabledTactics tauto
@@ -33,6 +33,7 @@ HiddenHint (A : Prop) (hA : A) : A =>
  "Du hast einen Beweis dafür in den *Annahmen*."

 NewTactics constructor assumption
+DisabledTactics tauto

 -- Statement
 --     "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."
@@ -34,6 +34,7 @@ HiddenHint (A : Prop) (hA : A) : A =>
  "Du hast einen Beweis dafür in den *Annahmen*."

 NewTactics constructor assumption
+DisabledTactics tauto

 -- Statement
 --     "Zeige $(A \\land (A \\Rightarrow B)) \\iff (A \\land B)$."
@@ -31,3 +31,4 @@ Hint (A : Prop) (B : Prop) (hA : A) : ¬ B =>
 "Sackgasse. Probier's nochmals."

 NewTactics left right assumption
+DisabledTactics tauto
@@ -45,3 +45,4 @@ Hint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
 "Jetzt noch das UND in den Annahmen mit `rcases h with ⟨h₁, h₂⟩` zerlegen."

 NewTactics assumption rcases
+DisabledTactics tauto
@@ -123,3 +123,4 @@ HiddenHint (A : Prop) (B : Prop) : A ∨ B =>
 "`left` oder `right`?"

 NewTactics left right assumption constructor rcases rfl contradiction trivial
+DisabledTactics tauto