Disp (grammar 0.3.0) next to Rust — same theme (Dark+ defaults), no color customizations

Same palette, same distribution: yellow application heads, light-blue variables/params/fields, blue declaration keywords and literals, purple control flow, teal types. Hover a token to see its scope.

// Hermetic (MODULES.md): prelude + raw earlier siblings; givens for forward types.
open use raw "../prelude.disp" {}
open use "../kernel/prelude.disp"
open given { Type : Type, Tree : Type, Unit : Type, Eq : Tree }

unit_val : Unit := t t t
one : Nat := 1
let teq_sig := checker_sig tree_eq
let nat_rec := nat_rec_fast

pred : Nat -> Nat :=
  {n} -> nat_rec ({_} -> Nat) 0 ({k, _prev} -> k) n

is_zero : Nat -> Bool :=
  {n} -> nat_rec ({_} -> Bool) true ({_k, _prev} -> false) n

guard (license_guard NatRecRelation.rel) nat_rec := nat_rec
guard (license_guard AddRelation.rel) add : Nat -> Nat -> Nat := {n, m} -> nat_rec ({_} -> Nat) m ({pred, ih} -> succ ih) n
guard freeze VERSION : Nat := 3

let x := if (is_derive (pair_fst tele)) then (m.recipe) else (field given (m.name))
verify : Module -> CheckerResult := {mod} -> match (apply_policed (mod.typ) (mod.record)) { Ok v => v; Err _ => Err }

test default_guard t (guard freeze (base zero)) = Ok (Both zero freeze)
test tree_eq (checker_sig pair_snd) pair_snd = false
test is_zero zero = true

pub(crate) fn drain(&mut self, budget: &mut i64) -> bool {
    let mut n: u64 = 0;
    let ok = loop {
        let Some((x, y)) = self.w.bag.pop() else { break true };
        if *budget <= 0 {
            break false;
        }
        *budget -= 1;
        n += 1;
        self.interact(x, y);
    };
    self.net.interactions.fetch_add(n, Ordering::Relaxed);
    ok
}