sed -ie "s/RhsPattern/ExpressionTerm/g"

h0nzZik · Jan 30, 2024 · 2f21c3c · 2f21c3c
1 parent aeb5db6
commit 2f21c3c
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -105,8 +105,8 @@ Section eqdec.
     Defined.
 
     #[export]
-    Instance RhsPattern_eqdec {Σ : StaticModel}
-        : EqDecision RhsPattern
+    Instance ExpressionTerm_eqdec {Σ : StaticModel}
+        : EqDecision ExpressionTerm
     .
     Proof.
         ltac1:(solve_decision).