Enable dynamic structuring by default

leanprover-community · Aug 7, 2024 · 0444234 · 0444234
1 parent 8ff1f48
commit 0444234
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/Aesop/Options/Public.lean b/Aesop/Options/Public.lean
@@ -162,7 +162,7 @@ structure Options where
 -/
 register_option aesop.dev.dynamicStructuring : Bool := {
   descr := "(aesop) Only for use by Aesop developers. Enables dynamic script structuring."
-  defValue := false
+  defValue := true
 }
 
 end Aesop
diff --git a/AesopTest/RulePattern.lean b/AesopTest/RulePattern.lean
@@ -44,8 +44,8 @@ axiom triangle (a b : Int) : |a + b| ≤ |a| + |b|
 
 example : |a + b| ≤ |c + d| := by
   aesop!
-  guard_hyp fwd_1  : |c + d| ≤ |c| + |d|
-  guard_hyp fwd    : |a + b| ≤ |a| + |b|
+  guard_hyp fwd   : |c + d| ≤ |c| + |d|
+  guard_hyp fwd_1 : |a + b| ≤ |a| + |b|
   falso
 
 @[aesop safe apply (pattern := (0 : Nat))]