From 2f21c3c68dee7046ea7705e61aa4f6e9c25eab33 Mon Sep 17 00:00:00 2001
From: Jan Tusil <jenda.tusil@gmail.com>
Date: Tue, 30 Jan 2024 11:32:50 +0100
Subject: [PATCH] sed -ie "s/RhsPattern/ExpressionTerm/g"

---
 minuska/theories/naive_interpreter.v | 2 +-
 minuska/theories/spec_semantics.v    | 4 ++--
 minuska/theories/spec_syntax.v       | 4 ++--
 minuska/theories/syntax_properties.v | 4 ++--
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/minuska/theories/naive_interpreter.v b/minuska/theories/naive_interpreter.v
index e2aabb5a..e97703f4 100644
--- a/minuska/theories/naive_interpreter.v
+++ b/minuska/theories/naive_interpreter.v
@@ -100,7 +100,7 @@ Definition rewrite_with
 Lemma evaluate_rhs_pattern_correct
     {Σ : StaticModel}
     
-    (φ : RhsPattern)
+    (φ : ExpressionTerm)
     (ρ : Valuation)
     (g : GroundTerm)
     :
diff --git a/minuska/theories/spec_semantics.v b/minuska/theories/spec_semantics.v
index 9121a46a..3943dfa2 100644
--- a/minuska/theories/spec_semantics.v
+++ b/minuska/theories/spec_semantics.v
@@ -666,7 +666,7 @@ Instance Satisfies_asb_expr
 
 
 #[export]
-Instance Satisfies__GroundTerm__RhsPattern
+Instance Satisfies__GroundTerm__ExpressionTerm
     {Σ : StaticModel}
     {V var : Type}
     {_varED : EqDecision var}
@@ -680,7 +680,7 @@ Instance Satisfies__GroundTerm__RhsPattern
     Satisfies
         V
         GroundTerm
-        RhsPattern
+        ExpressionTerm
         var
 .
 Proof. apply _. Defined.
diff --git a/minuska/theories/spec_syntax.v b/minuska/theories/spec_syntax.v
index 80aa7fc2..40b9413a 100644
--- a/minuska/theories/spec_syntax.v
+++ b/minuska/theories/spec_syntax.v
@@ -147,7 +147,7 @@ Inductive SideCondition {Σ : StaticModel} :=
 | sc_constraint (c : AtomicProposition)
 .
 
-Definition RhsPattern {Σ : StaticModel} :=
+Definition ExpressionTerm {Σ : StaticModel} :=
     Term' symbol Expression
 .
 
@@ -158,7 +158,7 @@ Record RewritingRule {Σ : StaticModel}
 := mkRewritingRule
 {
     fr_from : SymbolicTerm ;
-    fr_to : RhsPattern ;
+    fr_to : ExpressionTerm ;
     fr_scs : list SideCondition ;
 }.
 
diff --git a/minuska/theories/syntax_properties.v b/minuska/theories/syntax_properties.v
index d00be93c..039c2389 100644
--- a/minuska/theories/syntax_properties.v
+++ b/minuska/theories/syntax_properties.v
@@ -105,8 +105,8 @@ Section eqdec.
     Defined.
 
     #[export]
-    Instance RhsPattern_eqdec {Σ : StaticModel}
-        : EqDecision RhsPattern
+    Instance ExpressionTerm_eqdec {Σ : StaticModel}
+        : EqDecision ExpressionTerm
     .
     Proof.
         ltac1:(solve_decision).