From 0444234b4216e944d5be2ce42a25d7410c67876f Mon Sep 17 00:00:00 2001
From: Jannis Limperg <jannis@limperg.de>
Date: Wed, 7 Aug 2024 18:38:06 +0200
Subject: [PATCH] Enable dynamic structuring by default

---
 Aesop/Options/Public.lean  | 2 +-
 AesopTest/RulePattern.lean | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Aesop/Options/Public.lean b/Aesop/Options/Public.lean
index 3d46411..d5fad53 100644
--- 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
index 0e79da6..99d57a3 100644
--- 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))]