### Maude: Equality Predicate Simplification Example

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha160.txt

Demonstrates the updated operational semantics of the initial equality predicate ('.=.') in Maude. This example shows how function symbols that are equationally-stable can participate in simplifications, even without the 'ctor' attribute.

```maude
fmod FOO is
  inc INITIAL-EQUALITY-PREDICATE .
  sort Foo .
  ops a b c 1 : -> Foo .
  op __ : Foo Foo -> Foo [assoc] .
  op _+_ : Foo Foo -> Foo [assoc comm] .
  op s : Foo Foo -> Foo [comm] .
  op f : Foo Foo -> Foo [assoc comm id: 1] .
  ops g h p : Foo -> Foo .
  var A B C D E W X Y Z : Foo .
  eq p(X) = g(h(X)) .
endfm

red g(X) .=. g(Y) .
reduce in FOO : g(X) .=. g(Y) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Bool: X .=. Y
```

--------------------------------

### Maude: Strategy to Expression View Mapping Example

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha164.txt

Demonstrates a bug in Maude's strategy to expr view mappings that previously caused an internal error when the mapping was not well-defined. This example shows the problematic syntax and the expected warning output.

```maude
sth STRIV is
  including TRIV .
  strat st @ Elt .
endsth

view BuggyView from STRIV to NAT is
  sort Elt to Nat .
  strat st to expr match N:Nat s.t. N:Nat == M:Nat . *** M is unbound
endv
```

--------------------------------

### Maude A- and AU-unification Optimization Example

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha133.txt

This example illustrates an optimization in Maude's A- and AU-unification where constraints on variables are propagated into their assignments. This prevents finitary problems from becoming infinitary after substitution, as shown by the provided fmod definition and unify command.

```maude
fmod ASSOC-LIST is
  sorts Elt Pair List .
  subsort Elt Pair < List .
  op __ : List List -> List [assoc] .
  op __ : Elt Elt -> Pair [assoc] .
  op rev : List -> List .
  vars A B C X Y Z : List .
  vars P Q R : Pair .
  vars E F G : Elt .
endfm

unify P =? X Y /\ A P =? P B .
```

--------------------------------

### Handle Indent and Space Commands at Line Start in LaTeX

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha155.txt

Fixes a bug where the 'i' (indent) and 's' (space) format commands were ignored at the beginning of a line in LaTeX output. This example shows a metalevel reduction where these commands might be relevant.

```Maude
red in META-LEVEL : upModule('NAT, false) .

```

--------------------------------

### Maude Identity Mapping Example in Renaming

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha139.txt

This Maude example illustrates identity mappings during operator renaming. The first fmod 'BAR' shows an identity mapping for the '_+_' operator, while 'BAZ' demonstrates a non-identity mapping due to a change in the gather pattern, which is not quietly ignored.

```maude
fmod FOO is
  sort Foo .
  op _+_ : Foo Foo -> Foo [gather (e E)] .
endfm

fmod BAR is
  inc FOO * (op _+_ : Foo Foo -> Foo to _+_ [gather (e E)]) .
endfm

fmod BAZ is
  inc FOO * (op _+_ : Foo Foo -> Foo  to _+_ [gather (E e)]) .
endfm
```

--------------------------------

### AU-Unification with Multiple Equations Example (Maude)

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha133.txt

Shows a Maude unification problem involving multiple equations. This example demonstrates how the optimization for AU-unification might miss an irredundant unifier when solving a system of equations if not handled carefully, particularly concerning identity assignments.

```maude
unify W X =? Y Z /\ W X =? a a .
```

--------------------------------

### Order-Sorted Unification Example (Maude)

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha133.txt

Demonstrates a Maude module 'FOO3' with sort declarations, subsorting, and operator definitions, followed by a unification problem. This illustrates a scenario where a general unifier might fail to subsume all necessary unifiers due to sorting.

```maude
fmod FOO3 is
  sorts Lo Hi .
  subsort Lo < Hi .
  op 1 : -> Hi .
  op __ : Hi Hi -> Hi [assoc id: 1] .
  op __ : Lo Lo -> Lo [ditto] .
vars W X : Lo .
vars Y Z : Hi .
endfm

unify W =? Y Z .
```

--------------------------------

### Maude: Equality Predicate with Unstable Symbol Example

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha160.txt

Illustrates a specific scenario of the updated operational semantics for the equality predicate ('.=.') in Maude. This example shows the predicate returning false when comparing a ground term with an unstable top symbol against a non-ground term with an equationally-stable top symbol.

```maude
red f(a, g(b), c) .=. h(X) .
```

--------------------------------

### AU-Unification Optimization Example (Maude)

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha133.txt

Presents a Maude module 'FOO' to illustrate an optimization for AU-unification aimed at eliminating redundant unifiers generated by the PIG-PUG algorithm. It includes a unification problem and shows the generated unifiers, highlighting redundancy when an identity element exists.

```maude
fmod FOO is
  sort Foo .
  ops 1 a : -> Foo .
  op __ : Foo Foo -> Foo [assoc id: 1] .
vars W X Y Z : Foo .
endfm

unify W X =? Y Z .
```

--------------------------------

### Maude Example: Extension Information Bug

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha137.txt

Illustrates a bug in the handling of extension information for iter symbols in Maude. This example shows a scenario where incorrect multiple solutions are produced.

```maude
mod UNINITIALIZED-BUG is
  protecting NAT .
  vars N M : Nat .
  crl [rwc] : s N => M if N => M [nonexec] .
endm

srew 3 using rwc{idle} .
```

--------------------------------

### Maude Strategy-Controlled Rewriting

Source: https://context7.com/maude-lang/maude/llms.txt

Explains how to use Maude's strategy language to define user-controlled rule application order. It provides examples of sequential application (`apply-seq`) and non-deterministic choice (`try-both`).

```maude
smod STRATEGY-EXAMPLE is
  sorts State .
  ops a b c : -> State .
  rl [r1] : a => b .
  rl [r2] : b => c .
  rl [r3] : a => c .

  strat apply-seq @ State .
  sd apply-seq := r1 ; r2 .

  strat try-both @ State .
  sd try-both := r1 | r3 .
endsm

srewrite [apply-seq] a .
-- Applies r1 then r2: a => b => c
-- Result: c

srewrite [try-both] a .
-- Non-deterministically applies r1 or r3
-- Result: b or c depending on strategy choice
```

--------------------------------

### Maude: INSTALL File Update

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha143.txt

Updates the INSTALL file with step-by-step instructions for building Maude on Linux and Mac operating systems.

```plaintext
The INSTALL file has been updated with step-by-step instructions for building on Linux and Mac.
```

--------------------------------

### Maude Identity Axiom Optimization Limitation Example

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha133.txt

This example showcases a limitation of Maude's identity axiom optimization. When the identity axiom is sort decreasing, the optimization is disabled. This snippet defines the FOO2 module with a sort-decreasing identity axiom and demonstrates how irredundant unification is necessary for completeness in order-sorted problems.

```maude
fmod FOO2 is
  sorts Lo Hi .
  subsort Lo < Hi .
  op 1 : -> Lo .
  op __ : Hi Hi -> Hi [assoc id: 1] .
vars W X Y Z : Lo .
endfm

unify W =? Y Z .
irred unify W =? Y Z .
```

--------------------------------

### Maude: Parameterized constants in modules

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha140.txt

Demonstrates how constants can be parameterized in Maude modules, similar to sorts. This example shows a constant 'c' within a module 'FOO' that is parameterized by 'X' and 'Y'. When imported into another module 'BAR', the constant instantiation mimics that of sorts.

```maude
fmod FOO{X :: TRIV, Y :: TRIV} is
  sort Foo{X,Y} .
  op c{X,Y} : -> Foo{X,Y} .
endfm

fmod BAR is
  inc FOO{Nat,String} .
endfm

red c{Nat,String} .

```

--------------------------------

### Maude Example: Loop Mode Bug

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha137.txt

Demonstrates a bug in Maude's loop mode where it inappropriately uses leftover state from a previous incompatible command. This search command provokes the issue.

```maude
search 0 =>* 0 .
```

--------------------------------

### Maude: Rewriting with Associative-Commutative Symbols

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha160.txt

Illustrates Maude's handling of associative-commutative symbols like '+'. The examples show how arguments are flattened and canceled when terms are unequal and non-ground, and how subterms are examined.

```maude
red g(A) + g(B) + g(C) .=. g(A) + B + h(C) .
reduce in FOO : g(A) + B + h(C) .=. g(A) + g(B) + g(C) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Bool: false

red g(A) + g(B) + g(C) .=. g(A) + B .
reduce in FOO : B + g(A) .=. g(A) + g(B) + g(C) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Bool: B .=. g(B) + g(C)
```

--------------------------------

### Maude Message Mapping Example (with Attributes)

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha139.txt

Illustrates a message mapping in Maude that includes an optional attribute list. The attribute list is converted to regular operator mappings during the canonicalization process.

```Maude
msg ⟨identifier⟩ to ⟨identifier⟩ [⟨attribute-list⟩]
```

--------------------------------

### Maude: Rewriting with Equationally-Stable Symbols

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha160.txt

Demonstrates rewriting in Maude using an equationally-stable function symbol 's'. This example shows how terms headed by such symbols are handled, specifically when arguments can be canceled.

```maude
reduce in FOO : h(X) .=. f(a, c, g(b)) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Bool: false

red s(g(X), Z) .=. s(Y, g(X)) .
reduce in FOO : s(Z, g(X)) .=. s(Y, g(X)) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Bool: Z .=. Y
```

--------------------------------

### Maude: Operator Renaming in Module

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha139.txt

Example showcasing a scenario with module importation and operator renaming in Maude. The code demonstrates how an operator 'f' is declared in a parameter module 'T' and then potentially renamed in a dependent module 'N'. This example was used to identify a spurious advisory bug.

```maude
fth T is
  sort S .
  op f : S -> S .
endfth

fmod M{X :: T} is
  sort V{X} .
  op f : V{X} -> V{X} .
endfm

fmod N{X :: T} is
  inc M{X} * (op f : V{X} -> V{X} to g) .
endfm
```

--------------------------------

### Maude: Parameterized classes in object-oriented syntax

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha140.txt

Demonstrates parameterization in Maude's object-oriented syntactic sugar, specifically with parameterized classes. This example shows a class 'Container{X}' within an object module 'CONTAINER' that is parameterized by 'X' and has a 'guts' attribute of type 'List{X}'.

```maude
omod CONTAINER{X :: TRIV} is
  pr LIST{X} .
  class Container{X} | guts : List{X} .
... 
endom

```

--------------------------------

### Handling Missing Tokens in Maude View Mappings

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha142.txt

Illustrates how Maude's parser handles missing '->' tokens in constant mappings within views and renamings. The example shows a view definition and a corresponding functional module instantiation, highlighting potential parsing behavior.

```maude
view FOO from DEFAULT to NAT is
  sort Elt to Nat .
  op 0 : Nat to 0 .
endv

fmod FOO is
  inc NAT * (op 0 : Nat to zero) .
endfm
```

--------------------------------

### Maude LTL Model Checking

Source: https://context7.com/maude-lang/maude/llms.txt

Demonstrates LTL model checking in Maude for verifying properties of state transition systems. It includes examples of checking temporal logic formulas like "always eventually in critical section".

```maude
load model-checker.maude

mod MUTEX is
  sorts State .
  ops idle wait crit : -> State .

  rl [enter] : idle => wait .
  rl [acquire] : wait => crit .
  rl [release] : crit => idle .
endm

mod MUTEX-CHECK is
  protecting MUTEX .
  including LTL+ .
  including MODEL-CHECKER+ .

  subsort State < State .

  op inCrit : -> Prop .
  eq < crit > |= inCrit = true .
  eq < S:State > |= inCrit = false [owise] .
endm

red modelCheck(idle, [] <> inCrit) .
-- Checks: "always eventually in critical section"
-- Returns: true or counterexample trace

red modelCheck(idle, [] (inCrit -> <> ~ inCrit)) .
-- Checks: "critical section always eventually exited"
-- LTL operators: [], <>, ->, /\, \/, ~, U, R
```

--------------------------------

### Maude Message Mapping Example (Typed)

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha139.txt

Shows a typed message mapping in Maude, specifying input types and return type for the message. This syntax is also converted to regular operator mappings during canonicalization.

```Maude
msg ⟨identifier⟩ : ⟨type-list⟩ -> <type> to ⟨identifier⟩ [<attribute-list>]
```

--------------------------------

### Maude Computation Commands with LaTeX Support

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha150.txt

Examples of computation-related Maude commands that are supported for LaTeX log generation. These commands perform calculations or state modifications and their output can be captured in LaTeX format.

```maude
reduce in <module> : <term> .
```

```maude
rewrite [<count>] in <module> : <term> .
```

```maude
frewrite [<count>,<gas>] in <module> : <term> .
```

```maude
erewrite [<count>,<gas>] in <module> : <term> .
```

```maude
continue .
```

--------------------------------

### Maude: Fix orphaned module purging

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha142.txt

This example highlights a bug where constructed modules orphaned by view replacements were not immediately purged from the module cache. The fix ensures timely cleanup of these modules, improving cache management.

```Maude
view V from TRIV + TRIV * (sort Elt to Elt2) to NAT + FLOAT is
  sort Elt to Nat .
  sort Elt2 to Float .
endv

show modules .

view V from TRIV to NAT is
  sort Elt to Nat .
endv

show modules .

fmod FOO is endfm

show modules .
```

--------------------------------

### Maude: Pseudo-parameter capture in module instantiation

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha144.txt

This snippet addresses a family of bugs where an identifier that looks like a parameter is captured by an actual parameter, leading to inconsistencies in module instantiation. It includes examples of pseudo-parameterization with sorts, constants, subsort declarations, and views.

```Maude
fmod FOO is
  sort Foo{X} .
endfm

fmod BAR{X :: TRIV} is
  inc FOO .
  op a : -> Foo{X} .
endfm

fmod BAZ{Y :: TRIV} is
  inc BAR{Y} .
endfm

-- Here the X in Foo{X} is not a parameter, but looks like a parameter.
-- We call such instantances pseudo-parameters. When FOO is imported
-- into BAR, Foo{X} comes within the scope of an actual parameter X.
-- When such a parameter is instantiated, say by a bound parameter Y,
-- as in this example, Foo{X} becomes Foo{Y} for uses of Foo{X} in BAR
-- but FOO is unparameterized so Foo{X} is imported uninstantiated, leading
-- to a missing sort and an internal error.

-- The same problem occurs:
-- (a) For a pseudo-parameterized constant c{X}.
-- (b) For other uses of the pseudo-parameterized entity such as subsort
--     declarations or statements.
-- (c) For instantiation by a view.
-- (d) Where the pseudo-parameter arises in an entirely benign way such as
--     Nat in Set{Nat} in the instantiation SET{Nat}.

-- The details of the internal error vary between various combinations
-- of these alternatives but the system is then unstable, even if it doesn't
-- immediately crash.

-- A related situation is where a module with a pseudo-parameter X is
-- instantiated by an actual parameter X from enclosing module:

fmod FOO{Y :: TRIV} is
  sort Foo{X} .
endfm

fmod BAR{X :: TRIV} is
  inc FOO{X} .
  sort Bar{X} .
  subsort Foo{X} < Bar{X} .
endfm

fmod BAZ{Z :: TRIV} is
  inc  BAR{Z} .
endfm

-- Something similar can happen if the actual parameter X comes from an
-- enclosing view:

fmod FOO{Y :: TRIV} is
  sort Foo{X} .
endfm

view V{X :: TRIV} from TRIV to FOO{X} is
  sort Elt to Foo{X} .
endv

fmod BAR{Z :: TRIV} is
  inc SET{V{Z}} .
endfm

-- More complex captures are possible; for example by instantiating
-- with a view instance that has a bound parameter X, as in:

fmod M{X :: TRIV} is
  sort S{X} .
endfm

view V{X :: TRIV} from TRIV to M{X} is
  sort Elt to S{X} .
endv

fmod FOO{Y :: TRIV} is
  sort Foo{X} .
endfm

fmod BAR{X :: TRIV} is
  inc FOO{V{X}} .
  op a : -> Foo{X} .
endfm

fmod BAZ is
  inc BAR{Nat} .
endfm

-- Or even:

fmod M{X :: TRIV} is
  sort S{X} .
endfm

view V{X :: TRIV} from TRIV to M{X} is
  sort Elt to S{X} .
endv

fmod M2{X :: TRIV} is
  sort S2{X} .
endfm

```

--------------------------------

### Maude Show Commands with LaTeX Support

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha150.txt

Examples of Maude 'show' commands for inspecting internal state that are supported for LaTeX log generation. These commands do not typically echo in the log but will when LaTeX output is enabled, with a blank line separating the command from its output.

```maude
show desugared <module> .
```

```maude
show processed <view> .
```

```maude
show all <module> .
```

```maude
show sorts <module> .
```

```maude
show mbs <module> .
```

```maude
show eqs <module> .
```

```maude
show rls <module> .
```

--------------------------------

### Maude Operator Mapping with Attributes

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha145.txt

Example of Maude operator mapping demonstrating overparsing for attributes like 'format' and 'prec' without providing the required information. This illustrates another parsing issue corrected in this release.

```Maude
fmod FOO is
  inc NAT * (op _+_ to _++_ [format prec gather]) .
endfm
```

--------------------------------

### Maude: Parsing Numeric Strings in Rat Operator

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha160.txt

Demonstrates a bug fix in the 'rat' operator within the CONVERSION module. Previously, it failed to correctly handle strings representing numbers with leading zeros or negative signs followed by zero. This example shows the corrected behavior.

```maude
Maude> red rat("-0", 10) .
reduce in CONVERSION : rat("-0", 10) .
rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
result [Rat,FindResult]: rat("-0", 10)
Maude> 
> red rat("0/1", 10) .
reduce in CONVERSION : rat("0/1", 10) .
rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
result [Rat,FindResult]: rat("0/1", 10)
Maude> 
> red rat("-0/1", 10) .
reduce in CONVERSION : rat("-0/1", 10) .
rewrites: 0 in 0ms cpu (0ms real) (~ rewrites/second)
result [Rat,FindResult]: rat("-0/1", 10)
```

--------------------------------

### Maude: Fix orphaned view instantiations in cache

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha142.txt

This example illustrates a bug where orphaned view instantiations were not deleted from the view cache. The fix ensures that unused views are properly removed, preventing related module instantiation cache issues.

```Maude
fmod FOO is
  inc LIST{Set{Nat}} .
endfm

show modules .
show views .

fmod FOO is
endfm

show modules .
show views .
```

--------------------------------

### Maude Timer Management Example

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha134.txt

This Maude module defines and executes a scenario involving three timers: one periodic and two one-shot. It illustrates timer creation, starting with specified durations and modes, handling time-out events, and stopping/deleting timers. The code utilizes Maude's built-in TIME and STD-STREAM modules.

```Maude
load time
load file

mod TEST is
  inc TIME .
  inc STD-STREAM .

  op myClass : -> Cid .
  ops me : -> Oid .
  op firstTimer : Oid -> Attribute .
  op secondTimer : Oid -> Attribute .
  op thirdTimer : Oid -> Attribute .
  op run : -> Configuration .
  eq run = <> < me : myClass | none > createTimer(timeManager, me) .

vars O O2 O3 O4 O5 : Oid .
var N : Nat .
  rl < O : myClass | none > createdTimer(O, O2, O3) =>
     < O : myClass | firstTimer(O3) > createTimer(timeManager, me) .
     
  rl < O : myClass | firstTimer(O3) > createdTimer(O, O2, O4) =>
     < O : myClass | firstTimer(O3), secondTimer(O4) > createTimer(timeManager, me) .

  rl < O : myClass | firstTimer(O3), secondTimer(O4) > createdTimer(O, O2, O5) =>
     < O : myClass | firstTimer(O3), secondTimer(O4), thirdTimer(O5) >
     startTimer(O3, me, periodic, 500 ms)
     startTimer(O4, me, oneShot, 1250 ms)
     startTimer(O5, me, oneShot, 3250 ms).

  rl < O : myClass | firstTimer(O3), secondTimer(O4), thirdTimer(O5) >
     timeOut(O, O3) =>
     < O : myClass | firstTimer(O3), secondTimer(O4), thirdTimer(O5) >
     write(stdout, O, "time out for first timer\n") .

  rl < O : myClass | firstTimer(O3), secondTimer(O4), thirdTimer(O5) >
     timeOut(O, O4) =>
     < O : myClass | firstTimer(O3), secondTimer(O4), thirdTimer(O5) >
     write(stdout, O, "time out for second timer\n") .

  rl < O : myClass | firstTimer(O3), secondTimer(O4), thirdTimer(O5) >
     timeOut(O, O5) =>
     < O : myClass | firstTimer(O3), secondTimer(O4), thirdTimer(O5) >
     write(stdout, O, "time out for third timer\n")
     stopTimer(O3, O) .

  rl < O : myClass | firstTimer(O3), secondTimer(O4), thirdTimer(O5) >
     stoppedTimer(O, O3) =>
     < O : myClass | none >
     deleteTimer(O3, O) deleteTimer(O4, O) deleteTimer(O5, O) .
endm

erew run .
```

--------------------------------

### Maude: Add LaTeX support for 'get variants/get irredundant variants' commands

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha152.txt

Enables LaTeX output for Maude's 'get variants' and 'get irredundant variants' commands. This improves the formatting of variant information retrieval.

```Maude
get variants ...
get irredundant variants ...

```

--------------------------------

### Maude Timer Starting Message Format

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha134.txt

Specifies the message format for starting a timer in Maude. The `startTimer` message requires the Oid of the timer, the Oid of the time manager, a `TimerMode` (oneShot or periodic), and a `NzNat` for the countdown duration. The `startedTimer` message confirms the timer has started.

```Maude
op startTimer : Oid Oid TimerMode NzNat -> Msg [ctor msg format (b o)] .
op startedTimer : Oid Oid -> Msg [ctor msg format (m o)] .
```

--------------------------------

### Improved Pretty Printing Example (Maude)

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha153.txt

Illustrates an improvement in Maude's pretty-printing logic for statements. It shows how the system now infers the kind of overloaded terms like '0' based on context (e.g., left-hand sides of assignment, implication, or mapping), reducing the need for explicit sort disambiguation.

```Maude
mod FOO is
  sorts Foo Bar .
  ops a b 0 : -> Foo .
  op 0 : -> Bar .
  cmb 0 : Bar if 0 : Foo .
  ceq a = 0 if b = 0 .
  crl b => 0 if a => 0 /\ b := 0 .
endm

show desugared .
```

--------------------------------

### Maude Module System and Parameterization

Source: https://context7.com/maude-lang/maude/llms.txt

Illustrates Maude's module system, focusing on parameterized modules, theories, and views for generic programming. It shows how to define a parameterized list module and instantiate it with a specific type.

```maude
fth TRIV is
  sort Elt .
endfth

fmod LIST{X :: TRIV} is
  sort List{X} .
  subsort X$Elt < List{X} .

  op nil : -> List{X} [ctor] .
  op _;_ : List{X} List{X} -> List{X} [ctor assoc id: nil] .
  op reverse : List{X} -> List{X} .

  var E : X$Elt .
  var L : List{X} .

  eq reverse(nil) = nil .
  eq reverse(E ; L) = reverse(L) ; E .
endfm

view Nat from TRIV to NAT is
  sort Elt to Nat .
endv

-- Instantiate parameterized module
fmod NAT-LIST is
  protecting LIST{Nat} .
endfm

red in NAT-LIST : reverse(s 0 ; s s 0 ; s s s 0) .
-- Result: s s s 0 ; s s 0 ; s 0
```

--------------------------------

### Vu-Narrow Command Syntax

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha132.txt

Illustrates the new syntax for the 'vu-narrow' command, which supports optional narrowing options, variant unification options, solution limits, depth bounds, and module specification. This provides a more flexible and powerful way to perform narrowing operations.

```maude
debug {<narrowing options>} vu-narrow
  {<variant unification options>}
  [<nr-solutions>, <depth-bound>]
  in <module> :
  <term> <search-type> <term> .
```

--------------------------------

### Meta-Interpreter Error Message Example (Maude)

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha133.txt

Provides an example of an 'interpreterError()' message returned by a Maude meta-interpreter. This message format is used to report erroneous input to the meta-interpreter, ensuring consistent error handling across different execution environments.

```maude
interpreterError(me, interpreter(0), "Bad type.")
```

--------------------------------

### Maude Show Desugared Commands

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha138.txt

Introduces new commands, `show desugared .` and `show desugared <module> .`, for displaying modules after syntactic sugar removal. These commands show explicit imports and analyze the module structure.

```Maude
show desugared .
show desugared <module> .
```

--------------------------------

### Maude vu-narrow with path and fold options

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha161.txt

Illustrates the combined usage of 'path' and 'fold' options with the vu-narrow command in Maude. This advanced usage allows for path locking and folding, enabling more complex state management during narrowing.

```Maude
{path,fold} vu-narrow {filter,delay} g(j(A, B)) =>* C .

```

--------------------------------

### Maude Message Mapping Example (Simple)

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha139.txt

Defines a simple message mapping in Maude, renaming a message identifier to another. This syntax is converted to regular operator mappings during canonicalization.

```Maude
msg ⟨identifier⟩ to ⟨identifier⟩
```

--------------------------------

### Maude: Meta-Level Object Constructor Parsing

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha139.txt

Illustrates the use of metaParse at the meta-level in Maude to parse an object constructor with omitted attribute set identity. This demonstrates the syntactic sugar feature working in the meta-level environment, translating the simplified syntax into its desugared form.

```maude
red in META-LEVEL : metaParse(upModule('CONFIGURATION, false),
'< 'O:Oid ': 'C:Cid '| '>
, anyType) .
reduce in META-LEVEL : metaParse(upModule('CONFIGURATION, false), '< 'O:Oid ': 'C:Cid '| '>, anyType) .
rewrites: 3 in 0ms cpu (0ms real) (~ rewrites/second)
result ResultPair: {'<_:_|_>['O:Oid,'C:Cid,'none.AttributeSet],'Object}
```

--------------------------------

### LaTeX Support for Show Module (Maude)

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha153.txt

Details the added LaTeX support for `show mod <module name>` and `show module <module name>`. This feature displays unparsed modules, rendering hooks, identity terms, axioms, equations, rules, and strategy definitions as text bubbles using `\maudeRaw{}`. Parameterized sorts and constants in renamings are printed naively using `\maudeSort{}`.

```Maude
show module FOO .
show mod FOO .
```

--------------------------------

### Maude: 'show desugared' command output for imports

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha140.txt

Illustrates a bug fix in the 'show desugared' command for Maude. The fix addresses an issue where imported modules with parameters were printed with extraneous '[]' characters around bound parameters due to internal caching mechanisms. This example shows the corrected output format.

```maude
show desugared LIST-AND-SET .

fmod LIST-AND-SET{X :: TRIV} is
  protecting LIST{[X]} .
  protecting SET{[X]} .
  : 
endfm

```

--------------------------------

### Maude: Module instantiation with parameterized constants and renamings

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha144.txt

This snippet illustrates a bug fix in Maude concerning the correct instantiation of modules with bound parameters when renamings are involved. It specifically addresses issues with parameterized constants and object-oriented renamings.

```Maude
fmod FOO{X :: TRIV} is
  sort Foo{X} .
  op f{X} : -> Foo{X} .
endfm

fmod BAR{X :: TRIV} is
  pr FOO{X} * (op f{X} to g) .
  eq g = g .
endfm

fmod TEST is
  inc BAR{Nat} .
endfm

show all .

ASSERT FAILED: ../../../src/Mixfix/importTranslation.cc:401
no translation for g in TEST was looking for g
Aborted (core dumped)

-- Here the renaming in the instantiation,
--   fmod FOO{Nat} * (op f`{Nat`} to g)
-- was not being created as an instantiation of (op f{X} to g).

-- This also affected object-oriented renamings:

omod FOO{X :: TRIV} is
  class Foo{X} .
endom

omod BAR{X :: TRIV} is
  inc FOO{X} * (class Foo{X} to Bar{X}) .
  op className : -> Cid .
  eq className = Bar{X} .
endom

omod TEST is
  inc BAR{Nat} .
endom

show all .

```

--------------------------------

### Maude: vu-narrow Unsafe Name Handling

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha160.txt

Illustrates a bug fix in 'vu-narrow' and 'fvu-narrow' that previously allowed unsafe names like '#1:Foo' at both object and meta levels. This code shows the module definition and the problematic usage.

```maude
mod FOO is
  sort Foo .
endm

vu-narrow #1:Foo =>* X:Foo .
vu-narrow X:Foo =>* #1:Foo .
```

--------------------------------

### Maude Self-Check Failure Message

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha144.txt

An example of a self-check failure message in Maude, indicating an issue with renaming a sort within a module instantiation. This message is used for debugging and reporting bugs.

```text
ASSERT FAILED: ../../../src/Mixfix/renameModule.cc:131
couldn't find sort Foo{Z} renamed from Foo{X} in module BAR{[Z]}
Aborted (core dumped)
```

--------------------------------

### Maude Operator Declaration with Attributes

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha145.txt

Example of Maude operator declaration showing overparsing for multiple attributes without necessary information. This highlights a potential parsing issue addressed in the release.

```Maude
fmod FOO is
  op _+_ : Bool Bool -> Bool [prec gather format strat strategy poly] .
endfm
```

--------------------------------

### Parameterize Module with System Theory from Oth in Maude

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha140.txt

Demonstrates how a system module (omod) can be parameterized by system theories generated from object-oriented theories (oths). The parameters G and R are specified as CONTAINER, which is likely an oth.

```maude
omod TRANSFER{G :: CONTAINER, R :: CONTAINER} is
...
endom
```

--------------------------------

### Maude: vu-narrow with Disjunction of Initial States

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha160.txt

Shows the usage of the 'vu-narrow' command in Maude with a disjunction of initial states. It highlights the support for multiple search types and restrictions on variable sharing between states and patterns.

```maude
mod FOO is
  sort Foo .
  ops a a2 b b2 f g : Foo -> Foo .
vars P Q R S T X : Foo .
  rl a(f(X)) => a2(X) [narrowing] .
  rl b(g(X)) => b2(X) [narrowing] .
endm

vu-narrow a(P) \/ b(Q) =>* a2(R) .
vu-narrow in FOO : a(P) \/ b(Q) =>* a2(R) .

```

--------------------------------

### Parameterizing Modules with pconst Constants in Views

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha141.txt

Demonstrates the new capability to use constants with the `pconst` attribute on both sides of op to term mappings in views, enabling module parameterization by terms.

```maude
fth NAT-ARG is
  inc NAT .
  op arg : -> Nat [pconst] .
endfth

fmod GAME-OF-LIFE{X :: NAT-ARG, Y :: NAT-ARG} is
...
endfm

view 42 from NAT-ARG to NAT is
  op arg to term 42 .
endv

fmod TEST is
  inc GAME-OF-LIFE{42, 42} .
endfm
```

--------------------------------

### Maude Class Mapping Example

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha139.txt

Demonstrates a class mapping in Maude, which renames a class C to D. This transformation generates both a sort renaming and an operator renaming, effectively aliasing the class and its associated operator.

```Maude
class C to D

-- This generates:
-- sort C to D
-- op C : -> [C] to D
```

--------------------------------

### Maude Statement Transformation Example

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha139.txt

Illustrates a rule (rl) statement in Maude that undergoes transformation. The `[dnt]` attribute prevents further transformation of this specific rule, ensuring it's passed directly to the system module.

```maude
rl < O : C | > => < O : C' | > [dnt] .  *** change class of object O
```

--------------------------------

### Maude: 'set generate-by' Command Addition

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha143.txt

Introduces the 'set generate-by <Module> <polarity>' command to provide symmetry with other importation modes. An example demonstrates its usage with the NAT module and a module FOO.

```maude
The is a command
  set generate-by <Module> <polarity> .
for symmetry with the the other 3 importation modes.

Maude> set generate-by NAT on .
Maude> fmod FOO is endfm
Maude> show desugared FOO .
fmod FOO is
  including BOOL .
  generated-by NAT .
endfm

This asymmetry in the design was noticed by Rubén.
```

--------------------------------

### Maude: Meta-Level Module Up

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha139.txt

Illustrates the meta-level operation to 'upModule' for a Maude theory. This function is used to get the internal representation of a module. The output reveals an incorrect inclusion of 'BOOL', indicating a bug fix in this release.

```maude
Maude> red in META-LEVEL : upModule('FOO, false) .
reduce in META-LEVEL : upModule('FOO, false) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result FTheory: fth 'FOO is
  including 'BOOL .
  sorts 'Foo .
  none
  none
  none
  none
endfth
```

--------------------------------

### Maude: Parsing special tokens and operators

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha144.txt

This snippet demonstrates Maude's handling of special tokens that start with a quote but are not strings, and the application of iterated operators. It shows how Maude parses and reduces expressions involving these constructs.

```Maude
fmod FOO is
  pr NAT .
  op "s" : Nat -> Nat [iter] .
  op "f"g : Nat -> Nat [iter] .
endfm

red "X":Nat .
red "X:Y":NzNat .
red "X:Y"Z:NzNat .
red "X":[Nat] .

red "s"^42(0) .
red "f"g^2(0) .

```

--------------------------------

### Maude: Rewriting with Associative Symbols

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha160.txt

Demonstrates Maude's approach to associative symbols, focusing on decomposing argument lists by pairing fixed subterms. It covers scenarios where subterms have different symbols and how remaining lists are handled.

```maude
red g(A) (B) X h(A) Y h(C) .=. h(A) g(D) g(E) Z X h(A) .
reduce in FOO : g(A) B X h(A) Y h(C) .=. h(A) g(D) g(E) Z X h(A) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Bool: false

red g(A) X Y h(A) h(C) .=. g(D) g(E) g(D) X h(A) .
reduce in FOO : g(A) X Y h(A) h(C) .=. g(D) g(E) g(D) X h(A) .
rewrites: 1 in 0ms cpu (0ms real) (~ rewrites/second)
result Bool: false

red g(A) g(B) X h(A) Y h(C) .=. g(D) g(E) Z X h(A) .
reduce in FOO : g(A) g(B) X h(A) Y h(C) .=. g(D) g(E) Z X h(A) .
rewrites: 4 in 0ms cpu (0ms real) (~ rewrites/second)
result Bool: E .=. B and A .=. C and A .=. D and Z X .=. X h(A) Y
```

--------------------------------

### Maude Directory API: Entry Types and Messages

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha136.txt

Details the entry types within a directory (file, directory, socket, pipe, charDevice, blockDevice, symbolicLink) and the special `endOfDirectory` marker. It also lists the messages for interacting with directories, such as `openDirectory`, `closeDirectory`, `getDirectoryEntry`, `makeDirectory`, and `removeDirectory`.

```Maude
  ops file directory socket pipe charDevice blockDevice : -> EntryType [ctor] .
  op symbolicLink : String -> EntryType [ctor] .
  op endOfDirectory : -> EntryType? [ctor] .

  op openDirectory : Oid Oid String -> Msg [ctor msg format (b o)] .
  op openedDirectory : Oid Oid Oid -> Msg [ctor msg format (m o)] .
  op closeDirectory : Oid Oid -> Msg [ctor msg format (b o)] .
  op closedDirectory : Oid Oid -> Msg [ctor msg format (m o)] .
  op getDirectoryEntry : Oid Oid -> Msg [ctor msg format (b o)] .
  op gotDirectoryEntry : Oid Oid String EntryType? -> Msg [ctor msg format (m o)] .

  op makeDirectory : Oid Oid String -> Msg [ctor msg format (b o)] .
  op madeDirectory : Oid Oid -> Msg [ctor msg format (m o)] .
  op removeDirectory : Oid Oid String -> Msg [ctor msg format (b o)] .
  op removedDirectory : Oid Oid -> Msg [ctor msg format (m o)] .

  op directoryError : Oid Oid String -> Msg [ctor msg format (m o)] .

```

--------------------------------

### Maude Generic Attribute Mapping Example

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha139.txt

Illustrates a generic attribute mapping in Maude, renaming an attribute A to B. For each attribute operator A`:_ in the module being renamed, this generates a specific operator mapping to the new attribute name B`:_.

```Maude
attr A to B

-- For each attribute operator A`:_ : [K] -> Attribute in the module being renamed,
-- this generates:
-- op A`:_ : [K] -> Attribute to B`:_ 
```

--------------------------------

### Maude Operator Formatting with `format` Attribute

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha153.txt

Demonstrates how the `format` attribute in Maude controls spacing around tokens in mixfix syntax. The example shows two fmod declarations with different `format` attributes, illustrating the impact on output.

```maude
fmod FOO is
  sort Foo .
  op [_,_] : Foo Foo -> Foo [format (d d d d d d)] .
  ops a b c d e : -> Foo .
endfm

red [a, [[b, c], d]] .

fmod FOO is
  sort Foo .
  op [_,_] : Foo Foo -> Foo [format (d d d s d d)] .
  ops a b c d e : -> Foo .
endfm

red [a, [[b, c], d]] .
```

--------------------------------

### Bug Fix: Polymorphic Operator ctor Attribute (Maude)

Source: https://github.com/maude-lang/maude/blob/master/doc/alpha153.txt

Addresses a bug where the `ctor` attribute was not printed correctly for polymorphic operators in LaTeX output. The example demonstrates a polymorphic operator `f` declared with `poly (2) ctor`.

```Maude
fmod FOO is
  sort Foo .
  op f : Foo Universal -> Foo [poly (2) ctor] .
endfm

show desugared .
```