From 728345228b63fc7553b274571494d1a314e9f9f0 Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 12 Mar 2024 17:20:55 -0500 Subject: [PATCH 1/2] Remove uses of latex attribute --- 1_k/1_lambda/lesson_4/lambda.k | 2 +- 1_k/1_lambda/lesson_5/lambda.k | 2 +- 1_k/1_lambda/lesson_6/lambda.k | 2 +- 1_k/1_lambda/lesson_7/lambda.k | 2 +- 1_k/1_lambda/lesson_8/lambda.k | 4 ++-- 1_k/1_lambda/lesson_9/lambda.md | 4 ++-- 1_k/2_imp/lesson_1/imp.k | 2 +- 1_k/2_imp/lesson_2/imp.k | 2 +- 1_k/2_imp/lesson_3/imp.k | 2 +- 1_k/2_imp/lesson_4/imp.k | 2 +- 1_k/2_imp/lesson_5/imp.md | 2 +- 1_k/3_lambda++/lesson_1/lambda.k | 4 ++-- 1_k/3_lambda++/lesson_2/lambda.k | 2 +- 1_k/3_lambda++/lesson_3/lambda.k | 2 +- 1_k/3_lambda++/lesson_4/lambda.k | 2 +- 1_k/3_lambda++/lesson_5/lambda.k | 4 ++-- 1_k/3_lambda++/lesson_6/lambda.md | 7 ++----- 1_k/4_imp++/lesson_1/imp.k | 2 +- 1_k/4_imp++/lesson_2/imp.k | 2 +- 1_k/4_imp++/lesson_3/imp.k | 2 +- 1_k/4_imp++/lesson_4/imp.k | 2 +- 1_k/4_imp++/lesson_5/imp.k | 2 +- 1_k/4_imp++/lesson_6/imp.k | 2 +- 1_k/4_imp++/lesson_7/imp.k | 2 +- 1_k/4_imp++/lesson_8/imp.md | 2 +- 1_k/5_types/lesson_1/imp.k | 2 +- 2_languages/1_simple/1_untyped/simple-untyped.md | 5 ++--- .../1_simple/2_typed/2_dynamic/simple-typed-dynamic.md | 5 ++--- 2_languages/2_kool/1_untyped/kool-untyped.md | 4 ++-- 2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md | 5 ++--- 2_languages/2_kool/2_typed/2_static/kool-typed-static.md | 2 +- 31 files changed, 40 insertions(+), 46 deletions(-) diff --git a/1_k/1_lambda/lesson_4/lambda.k b/1_k/1_lambda/lesson_4/lambda.k index 0872c46e..ceff13db 100644 --- a/1_k/1_lambda/lesson_4/lambda.k +++ b/1_k/1_lambda/lesson_4/lambda.k @@ -5,7 +5,7 @@ module LAMBDA-SYNTAX imports ID-SYNTAX syntax Val ::= Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp syntax Exp ::= Val | Exp Exp [strict, left] | "(" Exp ")" [bracket] diff --git a/1_k/1_lambda/lesson_5/lambda.k b/1_k/1_lambda/lesson_5/lambda.k index dabe6857..74d308f8 100644 --- a/1_k/1_lambda/lesson_5/lambda.k +++ b/1_k/1_lambda/lesson_5/lambda.k @@ -5,7 +5,7 @@ module LAMBDA-SYNTAX imports ID-SYNTAX syntax Val ::= Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp syntax Exp ::= Val | Exp Exp [strict, left] | "(" Exp ")" [bracket] diff --git a/1_k/1_lambda/lesson_6/lambda.k b/1_k/1_lambda/lesson_6/lambda.k index 9d955cbf..a969a10e 100644 --- a/1_k/1_lambda/lesson_6/lambda.k +++ b/1_k/1_lambda/lesson_6/lambda.k @@ -5,7 +5,7 @@ module LAMBDA-SYNTAX imports ID-SYNTAX syntax Val ::= Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp syntax Exp ::= Val | Exp Exp [strict, left] | "(" Exp ")" [bracket] diff --git a/1_k/1_lambda/lesson_7/lambda.k b/1_k/1_lambda/lesson_7/lambda.k index 30d3f4c1..8b9a4775 100644 --- a/1_k/1_lambda/lesson_7/lambda.k +++ b/1_k/1_lambda/lesson_7/lambda.k @@ -5,7 +5,7 @@ module LAMBDA-SYNTAX imports ID-SYNTAX syntax Val ::= Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp syntax Exp ::= Val | Exp Exp [strict, left] | "(" Exp ")" [bracket] diff --git a/1_k/1_lambda/lesson_8/lambda.k b/1_k/1_lambda/lesson_8/lambda.k index 0f6d5cea..17392e29 100644 --- a/1_k/1_lambda/lesson_8/lambda.k +++ b/1_k/1_lambda/lesson_8/lambda.k @@ -5,7 +5,7 @@ module LAMBDA-SYNTAX imports ID-SYNTAX syntax Val ::= Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp syntax Exp ::= Val | Exp Exp [strict, left] | "(" Exp ")" [bracket] @@ -23,7 +23,7 @@ module LAMBDA-SYNTAX rule let X = E in E':Exp => (lambda X . E') E syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro] - | "mu" Id "." Exp [latex(\mu{#1}.{#2})] + | "mu" Id "." Exp rule letrec F:Id X = E in E' => let F = mu F . lambda X . E in E' endmodule diff --git a/1_k/1_lambda/lesson_9/lambda.md b/1_k/1_lambda/lesson_9/lambda.md index b8943a60..06beac8c 100644 --- a/1_k/1_lambda/lesson_9/lambda.md +++ b/1_k/1_lambda/lesson_9/lambda.md @@ -76,7 +76,7 @@ interleaved) order. The initial syntax of our λ-calculus: ```k syntax Val ::= Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp syntax Exp ::= Val | Exp Exp [left, strict] | "(" Exp ")" [bracket] @@ -123,7 +123,7 @@ and faster to execute. ```k syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro] - | "mu" Id "." Exp [latex(\mu{#1}.{#2})] + | "mu" Id "." Exp rule letrec F:Id X:Id = E in E' => let F = mu F . lambda X . E in E' endmodule ``` diff --git a/1_k/2_imp/lesson_1/imp.k b/1_k/2_imp/lesson_1/imp.k index c774a804..eea0a9d1 100644 --- a/1_k/2_imp/lesson_1/imp.k +++ b/1_k/2_imp/lesson_1/imp.k @@ -8,7 +8,7 @@ module IMP-SYNTAX | "(" AExp ")" [bracket] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/2_imp/lesson_2/imp.k b/1_k/2_imp/lesson_2/imp.k index 8e1660b7..63847011 100644 --- a/1_k/2_imp/lesson_2/imp.k +++ b/1_k/2_imp/lesson_2/imp.k @@ -8,7 +8,7 @@ module IMP-SYNTAX | "(" AExp ")" [bracket] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/2_imp/lesson_3/imp.k b/1_k/2_imp/lesson_3/imp.k index 96f05e43..0247aa75 100644 --- a/1_k/2_imp/lesson_3/imp.k +++ b/1_k/2_imp/lesson_3/imp.k @@ -8,7 +8,7 @@ module IMP-SYNTAX | "(" AExp ")" [bracket] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/2_imp/lesson_4/imp.k b/1_k/2_imp/lesson_4/imp.k index 3fc116bf..b4d156a8 100644 --- a/1_k/2_imp/lesson_4/imp.k +++ b/1_k/2_imp/lesson_4/imp.k @@ -8,7 +8,7 @@ module IMP-SYNTAX | "(" AExp ")" [bracket] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/2_imp/lesson_5/imp.md b/1_k/2_imp/lesson_5/imp.md index 26a0a1b8..6f013855 100644 --- a/1_k/2_imp/lesson_5/imp.md +++ b/1_k/2_imp/lesson_5/imp.md @@ -33,7 +33,7 @@ argument, because we want to give it a short-circuit semantics. | "(" AExp ")" [bracket] > AExp "+" AExp [left, strict, color(pink)] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2}), color(pink)] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict, color(pink)] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1), color(pink)] diff --git a/1_k/3_lambda++/lesson_1/lambda.k b/1_k/3_lambda++/lesson_1/lambda.k index 10bd8800..f1f146c0 100644 --- a/1_k/3_lambda++/lesson_1/lambda.k +++ b/1_k/3_lambda++/lesson_1/lambda.k @@ -7,7 +7,7 @@ module LAMBDA-SYNTAX imports KVAR-SYNTAX syntax Val ::= KVar - | "lambda" KVar "." Exp [binder, latex(\lambda{#1}.{#2})] + | "lambda" KVar "." Exp [binder] syntax Exp ::= Val | Exp Exp [strict, left] | "(" Exp ")" [bracket] @@ -25,7 +25,7 @@ module LAMBDA-SYNTAX rule let X = E in E':Exp => (lambda X . E') E syntax Exp ::= "letrec" KVar KVar "=" Exp "in" Exp [macro] - | "mu" KVar "." Exp [binder, latex(\mu{#1}.{#2})] + | "mu" KVar "." Exp [binder] rule letrec F:KVar X = E in E' => let F = mu F . lambda X . E in E' syntax Exp ::= "callcc" Exp [strict] diff --git a/1_k/3_lambda++/lesson_2/lambda.k b/1_k/3_lambda++/lesson_2/lambda.k index c684fbee..b24d3b00 100644 --- a/1_k/3_lambda++/lesson_2/lambda.k +++ b/1_k/3_lambda++/lesson_2/lambda.k @@ -3,7 +3,7 @@ module LAMBDA imports DOMAINS syntax Exp ::= Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp | Exp Exp [strict, left] | "(" Exp ")" [bracket] diff --git a/1_k/3_lambda++/lesson_3/lambda.k b/1_k/3_lambda++/lesson_3/lambda.k index 3b52935f..d2f1f3cc 100644 --- a/1_k/3_lambda++/lesson_3/lambda.k +++ b/1_k/3_lambda++/lesson_3/lambda.k @@ -3,7 +3,7 @@ module LAMBDA imports DOMAINS syntax Exp ::= Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp | Exp Exp [strict, left] | "(" Exp ")" [bracket] diff --git a/1_k/3_lambda++/lesson_4/lambda.k b/1_k/3_lambda++/lesson_4/lambda.k index 7802a038..ed16cf14 100644 --- a/1_k/3_lambda++/lesson_4/lambda.k +++ b/1_k/3_lambda++/lesson_4/lambda.k @@ -3,7 +3,7 @@ module LAMBDA imports DOMAINS syntax Exp ::= Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp | Exp Exp [strict, left] | "(" Exp ")" [bracket] diff --git a/1_k/3_lambda++/lesson_5/lambda.k b/1_k/3_lambda++/lesson_5/lambda.k index d51ecb3d..bd867e19 100644 --- a/1_k/3_lambda++/lesson_5/lambda.k +++ b/1_k/3_lambda++/lesson_5/lambda.k @@ -10,7 +10,7 @@ module LAMBDA syntax Exp ::= Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp | Exp Exp [strict, left] | "(" Exp ")" [bracket] @@ -46,7 +46,7 @@ module LAMBDA rule let X = E in E':Exp => (lambda X . E') E syntax Exp ::= "letrec" Id Id "=" Exp "in" Exp [macro] - | "mu" Id "." Exp [latex(\mu{#1}.{#2})] + | "mu" Id "." Exp rule letrec F:Id X = E in E' => let F = mu F . lambda X . E in E' syntax Exp ::= muclosure(Map,Exp) diff --git a/1_k/3_lambda++/lesson_6/lambda.md b/1_k/3_lambda++/lesson_6/lambda.md index 664ac3a1..1c4554d4 100644 --- a/1_k/3_lambda++/lesson_6/lambda.md +++ b/1_k/3_lambda++/lesson_6/lambda.md @@ -39,7 +39,7 @@ We move all the LAMBDA++ syntax here. syntax Exp ::= Val // Basic lambda-calculus syntax | Id - | "lambda" Id "." Exp [latex(\lambda{#1}.{#2})] + | "lambda" Id "." Exp | Exp Exp [strict, left] | "(" Exp ")" [bracket] // Arithmetic @@ -52,7 +52,7 @@ We move all the LAMBDA++ syntax here. syntax Exp ::= "if" Exp "then" Exp "else" Exp [strict(1)] // Conditional | "let" Id "=" Exp "in" Exp [macro] // Let binder | "letrec" Id Id "=" Exp "in" Exp [macro] // Letrec - | "mu" Id "." Exp [latex(\mu{#1}.{#2})] // Mu + | "mu" Id "." Exp // Mu | "callcc" Exp [strict] // Callcc ``` @@ -108,7 +108,6 @@ then switch back to caller's environment. ```k syntax Val ::= closure(Map,Id,Exp) - [latex(\textsf{closure}_\lambda({#1},{#2},{#3}))] rule lambda X:Id . E => closure(Rho,X,E) ... Rho @@ -176,7 +175,6 @@ back to the fixed-point. ```k syntax Exp ::= muclosure(Map,Exp) - [latex(\textsf{closure}_\mu({#1},{#2}))] rule mu X . E => muclosure(Rho[X <- !N], E) ... Rho ... .Map => (!N:Int |-> muclosure(Rho[X <- !N], E)) ... @@ -192,7 +190,6 @@ supposed to be executed. Forget the environment, and you get a wrong ```k syntax Val ::= cc(Map,K) - [latex(\textsf{closure}_{\texttt{callcc}}({#1},{#2}))] rule (callcc V:Val => V cc(Rho,K)) ~> K Rho rule cc(Rho,K) V:Val ~> _ => V ~> K _ => Rho endmodule diff --git a/1_k/4_imp++/lesson_1/imp.k b/1_k/4_imp++/lesson_1/imp.k index fe043d01..276c5fd3 100644 --- a/1_k/4_imp++/lesson_1/imp.k +++ b/1_k/4_imp++/lesson_1/imp.k @@ -11,7 +11,7 @@ module IMP-SYNTAX > AExp "/" AExp [left, strict] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/4_imp++/lesson_2/imp.k b/1_k/4_imp++/lesson_2/imp.k index 13bc68b5..d6d5d23c 100644 --- a/1_k/4_imp++/lesson_2/imp.k +++ b/1_k/4_imp++/lesson_2/imp.k @@ -10,7 +10,7 @@ module IMP-SYNTAX > AExp "/" AExp [left, strict] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/4_imp++/lesson_3/imp.k b/1_k/4_imp++/lesson_3/imp.k index b62b77dd..c372b4e1 100644 --- a/1_k/4_imp++/lesson_3/imp.k +++ b/1_k/4_imp++/lesson_3/imp.k @@ -10,7 +10,7 @@ module IMP-SYNTAX > AExp "/" AExp [left, strict] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/4_imp++/lesson_4/imp.k b/1_k/4_imp++/lesson_4/imp.k index 2229bde8..fd17672d 100644 --- a/1_k/4_imp++/lesson_4/imp.k +++ b/1_k/4_imp++/lesson_4/imp.k @@ -10,7 +10,7 @@ module IMP-SYNTAX > AExp "/" AExp [left, strict] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/4_imp++/lesson_5/imp.k b/1_k/4_imp++/lesson_5/imp.k index be51e7eb..0fec3978 100644 --- a/1_k/4_imp++/lesson_5/imp.k +++ b/1_k/4_imp++/lesson_5/imp.k @@ -9,7 +9,7 @@ module IMP-SYNTAX > AExp "/" AExp [left, strict] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/4_imp++/lesson_6/imp.k b/1_k/4_imp++/lesson_6/imp.k index 984ee014..17dad487 100644 --- a/1_k/4_imp++/lesson_6/imp.k +++ b/1_k/4_imp++/lesson_6/imp.k @@ -10,7 +10,7 @@ module IMP-SYNTAX > AExp "/" AExp [left, strict] > AExp "+" AExp [left, strict] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/4_imp++/lesson_7/imp.k b/1_k/4_imp++/lesson_7/imp.k index 23a9fd8e..18b6cb03 100644 --- a/1_k/4_imp++/lesson_7/imp.k +++ b/1_k/4_imp++/lesson_7/imp.k @@ -12,7 +12,7 @@ module IMP-SYNTAX > "spawn" Block > Id "=" AExp [strict(2)] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/4_imp++/lesson_8/imp.md b/1_k/4_imp++/lesson_8/imp.md index a0121409..96045f88 100644 --- a/1_k/4_imp++/lesson_8/imp.md +++ b/1_k/4_imp++/lesson_8/imp.md @@ -129,7 +129,7 @@ of statements surrounded by curly brackets. > "spawn" Block > Id "=" AExp [strict(2)] syntax BExp ::= Bool - | AExp "<=" AExp [seqstrict, latex({#1}\leq{#2})] + | AExp "<=" AExp [seqstrict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict(1)] diff --git a/1_k/5_types/lesson_1/imp.k b/1_k/5_types/lesson_1/imp.k index a01a5d7a..0d40d3f1 100644 --- a/1_k/5_types/lesson_1/imp.k +++ b/1_k/5_types/lesson_1/imp.k @@ -12,7 +12,7 @@ module IMP-SYNTAX > "spawn" Block [strict] > Id "=" AExp [strict(2)] syntax BExp ::= Bool - | AExp "<=" AExp [strict, latex({#1}\leq{#2})] + | AExp "<=" AExp [strict] | "!" BExp [strict] | "(" BExp ")" [bracket] > BExp "&&" BExp [left, strict] diff --git a/2_languages/1_simple/1_untyped/simple-untyped.md b/2_languages/1_simple/1_untyped/simple-untyped.md index e497b1aa..50ca9a1a 100644 --- a/2_languages/1_simple/1_untyped/simple-untyped.md +++ b/2_languages/1_simple/1_untyped/simple-untyped.md @@ -438,7 +438,7 @@ not mention these: the configuration context of the rule is automatically transformed to match the declared configuration structure. ```k - syntax KItem ::= "undefined" [latex(\bot)] + syntax KItem ::= "undefined" rule var X:Id; => .K ... Env => Env[X <- L] @@ -1147,8 +1147,7 @@ corresponding store lookup operation. The following operation initializes a sequence of locations with the same value: ```k - syntax Map ::= Int "..." Int "|->" K - [function, latex({#1}\ldots{#2}\mapsto{#3})] + syntax Map ::= Int "..." Int "|->" K [function] rule N...M |-> _ => .Map requires N >Int M rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M ``` diff --git a/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md b/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md index b0a20711..09fe4535 100644 --- a/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md +++ b/2_languages/1_simple/2_typed/2_dynamic/simple-typed-dynamic.md @@ -222,7 +222,7 @@ location and then never allow that type to change. The typed undefined values effectively assign both a type and an undefined value to a location. ```k - syntax KItem ::= undefined(Type) [latex(\bot_{#1})] + syntax KItem ::= undefined(Type) rule T:Type X:Id; => .K ... Env => Env[X <- L] @@ -578,8 +578,7 @@ Adds the corresponding depth to an array type ``` Sequences of locations. ```k - syntax Map ::= Int "..." Int "|->" K - [function, latex({#1}\ldots{#2}\mapsto{#3})] + syntax Map ::= Int "..." Int "|->" K [function] rule N...M |-> _ => .Map requires N >Int M rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M diff --git a/2_languages/2_kool/1_untyped/kool-untyped.md b/2_languages/2_kool/1_untyped/kool-untyped.md index 5c915c00..ef93ec12 100644 --- a/2_languages/2_kool/1_untyped/kool-untyped.md +++ b/2_languages/2_kool/1_untyped/kool-untyped.md @@ -381,7 +381,7 @@ object and method closures. The semantics below are taken verbatim from the untyped SIMPLE definition. ```k - syntax KItem ::= "undefined" [latex(\bot)] + syntax KItem ::= "undefined" rule var X:Id; => .K ... Env => Env[X <- L] @@ -583,7 +583,7 @@ from SIMPLE unchanged. syntax Map ::= Int "..." Int "|->" K - [function, latex({#1}\ldots{#2}\mapsto{#3})] + [function] rule N...M |-> _ => .Map requires N >Int M rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M ``` diff --git a/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md b/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md index 7cfd474b..71d43165 100644 --- a/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md +++ b/2_languages/2_kool/2_typed/1_dynamic/kool-typed-dynamic.md @@ -247,7 +247,7 @@ KOOL). syntax KResult ::= Vals - syntax KItem ::= undefined(Type) [latex(\bot_{#1})] + syntax KItem ::= undefined(Type) rule T:Type X:Id; => .K ... Env => Env[X <- L] @@ -402,8 +402,7 @@ KOOL). rule T:Type<_,Vs:Vals> => T[] rule T:Type<.Vals> => T - syntax Map ::= Int "..." Int "|->" K - [function, latex({#1}\ldots{#2}\mapsto{#3})] + syntax Map ::= Int "..." Int "|->" K [function] rule N...M |-> _ => .Map requires N >Int M rule N...M |-> K => N |-> K (N +Int 1)...M |-> K requires N <=Int M diff --git a/2_languages/2_kool/2_typed/2_static/kool-typed-static.md b/2_languages/2_kool/2_typed/2_static/kool-typed-static.md index 30d4b144..fbd872dc 100644 --- a/2_languages/2_kool/2_typed/2_static/kool-typed-static.md +++ b/2_languages/2_kool/2_typed/2_static/kool-typed-static.md @@ -891,7 +891,7 @@ is co-variant in the codomain and contra-variant in the domain). ## Generic operations which could be part of the **K** framework ```k - syntax KItem ::= stuck(K) [latex(\framebox{${#1}$})] + syntax KItem ::= stuck(K) syntax KItem ::= "discard" rule _:KResult ~> discard => .K From b5d2d2fba5023a7a8f45a4eddb71d88c8b8cdfae Mon Sep 17 00:00:00 2001 From: Guy Repta <50716988+gtrepta@users.noreply.github.com> Date: Tue, 12 Mar 2024 17:21:35 -0500 Subject: [PATCH 2/2] Add couple things to .gitignore --- .gitignore | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.gitignore b/.gitignore index ccb245d6..0080eeda 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,3 @@ *-kompiled +*.depend +*kore-exec.tar.gz