Replace deprecated tokens

runtimeverification · Feb 21, 2024 · 7ffe2d6 · 7ffe2d6
1 parent d06285e
commit 7ffe2d6
Show file tree

Hide file tree

Showing 13 changed files with 34 additions and 34 deletions.
diff --git a/1_k/1_lambda/lesson_2/README.md b/1_k/1_lambda/lesson_2/README.md
@@ -14,7 +14,7 @@ The `requires` keyword takes a `.k` file containing language features that
 are needed for the current definition, which can be found in the
 [k-distribution/include/kframework/builtin](../../../../include/kframework/builtin/README.md) folder.  Thus, the command
 
-    require "substitution.k"
+    requires "substitution.k"
 
 says that the subsequent definition of LAMBDA needs the generic substitution,
 which is predefined in file `substitution.k` under the folder

diff --git a/1_k/3_lambda++/lesson_1/lambda.k b/1_k/3_lambda++/lesson_1/lambda.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
+requires "substitution.md"
 
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX

diff --git a/1_k/5_types/lesson_1.9/lambda.k b/1_k/5_types/lesson_1.9/lambda.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
+requires "substitution.md"
 
 module LAMBDA
   imports DOMAINS

diff --git a/1_k/5_types/lesson_2/lambda.k b/1_k/5_types/lesson_2/lambda.k
@@ -1,6 +1,6 @@
 // Copyright (c) Runtime Verification, Inc. All Rights Reserved.
 
-require "substitution.md"
+requires "substitution.md"
 
 module LAMBDA
   imports DOMAINS

diff --git a/1_k/5_types/lesson_4/lambda.k b/1_k/5_types/lesson_4/lambda.k
@@ -4,7 +4,7 @@
 // uses both substitution and symbolic reasoning.
 // It is intended for documentation and academic purposes only.
 
-require "substitution.md"
+requires "substitution.md"
 
 module LAMBDA
   imports DOMAINS

diff --git a/1_k/5_types/lesson_7/lambda.k b/1_k/5_types/lesson_7/lambda.k
@@ -4,7 +4,7 @@
 // uses both substitution and symbolic reasoning.
 // It is intended for documentation and academic purposes only.
 
-require "substitution.md"
+requires "substitution.md"
 
 module LAMBDA
   imports DOMAINS

diff --git a/1_k/5_types/lesson_8/lambda.k b/1_k/5_types/lesson_8/lambda.k
@@ -4,7 +4,7 @@
 // uses both substitution and symbolic reasoning.
 // It is intended for documentation and academic purposes only.
 
-require "substitution.md"
+requires "substitution.md"
 
 module LAMBDA
   imports DOMAINS

diff --git a/1_k/5_types/lesson_9.5/lambda.k b/1_k/5_types/lesson_9.5/lambda.k
@@ -4,8 +4,8 @@
 // uses substitution, unification and symbolic reasoning.
 // It is intended for documentation and academic purposes only.
 
-require "unification.k"
-require "substitution.md"
+requires "unification.k"
+requires "substitution.md"
 
 module LAMBDA-SYNTAX
   imports DOMAINS-SYNTAX

diff --git a/1_k/5_types/lesson_9/lambda.k b/1_k/5_types/lesson_9/lambda.k
@@ -4,7 +4,7 @@
 // uses both unification and symbolic reasoning.
 // It is intended for documentation and academic purposes only.
 
-require "unification.k"
+requires "unification.k"
 
 module LAMBDA
   imports DOMAINS

diff --git a/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md b/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md
@@ -363,16 +363,16 @@ a constructor for function types:
 ## Additional Priorities
 
 ```k
-  syntax priorities @__FUN-UNTYPED-COMMON
-                  > apply
-                  > arith
-                  > _:=__FUN-UNTYPED-COMMON
-                  > let_in__FUN-UNTYPED-COMMON
-                    letrec_in__FUN-UNTYPED-COMMON
-                    if_then_else__FUN-UNTYPED-COMMON
-                  > _;__FUN-UNTYPED-COMMON
-                  > fun__FUN-UNTYPED-COMMON
-                  > datatype_=___FUN-UNTYPED-COMMON
+  syntax priority @__FUN-UNTYPED-COMMON
+                > apply
+                > arith
+                > _:=__FUN-UNTYPED-COMMON
+                > let_in__FUN-UNTYPED-COMMON
+                  letrec_in__FUN-UNTYPED-COMMON
+                  if_then_else__FUN-UNTYPED-COMMON
+                > _;__FUN-UNTYPED-COMMON
+                > fun__FUN-UNTYPED-COMMON
+                > datatype_=___FUN-UNTYPED-COMMON
 endmodule
 
 module FUN-UNTYPED-MACROS

diff --git a/2_languages/3_fun/1_untyped/2_substitution/fun-untyped.md b/2_languages/3_fun/1_untyped/2_substitution/fun-untyped.md
@@ -24,8 +24,8 @@ the reader should consult the emvironment-based definition of FUN.
 ## Syntax
 
 ```k
-require "substitution.md"
-//require "modules/pattern-matching.k"
+requires "substitution.md"
+//requires "modules/pattern-matching.k"
 
 module FUN-UNTYPED-COMMON
   imports DOMAINS-SYNTAX
@@ -123,16 +123,16 @@ module FUN-UNTYPED-COMMON
 ## Additional Priorities
 
 ```k
-  syntax priorities @__FUN-UNTYPED-COMMON
-                  > ___FUN-UNTYPED-COMMON
-                  > arith
-                  > _:=__FUN-UNTYPED-COMMON
-                  > let_in__FUN-UNTYPED-COMMON
-                    letrec_in__FUN-UNTYPED-COMMON
-                    if_then_else__FUN-UNTYPED-COMMON
-                  > _;__FUN-UNTYPED-COMMON
-                  > fun__FUN-UNTYPED-COMMON
-                  > datatype_=___FUN-UNTYPED-COMMON
+  syntax priority @__FUN-UNTYPED-COMMON
+                > ___FUN-UNTYPED-COMMON
+                > arith
+                > _:=__FUN-UNTYPED-COMMON
+                > let_in__FUN-UNTYPED-COMMON
+                  letrec_in__FUN-UNTYPED-COMMON
+                  if_then_else__FUN-UNTYPED-COMMON
+                > _;__FUN-UNTYPED-COMMON
+                > fun__FUN-UNTYPED-COMMON
+                > datatype_=___FUN-UNTYPED-COMMON
 endmodule
 
 module FUN-UNTYPED-MACROS

diff --git a/2_languages/4_logik/basic/logik.md b/2_languages/4_logik/basic/logik.md
@@ -178,7 +178,7 @@ one may devise techniques to detect non-termination in some cases,
 one cannot do it in general (same like for all Turing-complete
 languages).
 ```k
-require "unification.k"
+requires "unification.k"
 
 module LOGIK-COMMON
   imports DOMAINS-SYNTAX

diff --git a/2_languages/4_logik/extended/exercises/logik-extended/logik.k b/2_languages/4_logik/extended/exercises/logik-extended/logik.k
@@ -3,7 +3,7 @@
 // NOTE: this definition is not runnable as is.
 // It is intended for documentation and academic purposes only.
 
-require "unification.k"
+requires "unification.k"
 
 module LOGIK-COMMON
   imports DOMAINS-SYNTAX