docs: document echo/product OCaml pipeline integration + expand wiki (PRs #45–46)

- CHANGELOG.md: add echo OCaml pipeline block; fixed exhaustiveness bullets
- PROOF-NEEDS.md: TG-4 → LANDED; update rule counts (16→26 HasType, 31→57 Step); TG-10 coverage expanded to include echoAdd/echoEq/product
- PROOF-NARRATIVE.md: update HasType/Step rule lists; add §2.6 OCaml completeness table; add product/echoAdd/echoEq rows to §2.5 table; TG-4 → LANDED
- FEATURE-COVERAGE.md: add 9 echo/product rows; update coverage summary (27→36); date bump
- FORMAL-SEMANTICS.md: extend §1.2 BNF; add §1.5 extended types; add §3.16 echo/product typing rules; add §4.10 echo/product eval rules; renumber downstream sections
- STATE.a2ml: update session/last-updated/milestones/blockers/next-actions/maintenance-status
- tangle.directives.a2ml: date bump to 2026-06-14
- docs/echo-types-ocaml-pipeline.md: new developer wiki page for echo/product integration

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -5,9 +5,9 @@
 [metadata]
 project = "tangle"
 version = "0.2.0-dev"
-last-updated = "2026-06-05"
+last-updated = "2026-06-14"
 status = "active"
-session = "echo-types realignment + decidability + CI bootstrap — 2026-06-05"
+session = "echo OCaml pipeline complete (PR #45+#46) — 2026-06-14"
 
 [project-context]
 name = "Tangle"
@@ -30,27 +30,24 @@ milestones = [
   "DONE (TG-2): decidability — infer ≡ HasType, type uniqueness, Decidable instance",
   "DONE: reproducible Lean toolchain bootstrap (proofs/bootstrap-lean.sh) + SessionStart hook; CI consolidated onto it",
   "NEXT (TG-1): extend type safety to let-binding (full de Bruijn substitution)",
-  "NEXT: generalise echo to add/eq (needs a product/residue type in Ty)",
+  "DONE: generalise echo to add/eq — product type (Ty.prod), echoAdd/echoEq in Lean+OCaml (PR #45)",
   "NEXT: thread echo residue into TangleIR (coordinate with quandledb)",
-  "NEXT: full OCaml echo pipeline (ast/typecheck/eval/parser/pretty)",
+  "DONE: full OCaml echo pipeline (ast/typecheck/eval/parser/pretty) — PR #45; build fixed PR #46",
   "LATER (TG-3): OCaml typecheck.ml refines the Lean HasType spec",
   "LATER (TG-5/6/7): compositional rewriter preservation; WASM semantic preservation; braid-group eqBraids",
 ]
 
 [blockers-and-issues]
-issues = [
-  "DESIGN (open, user): echo value shape — uniform `echoVal (residue,result)` (faithful to Echo=Σ, reworks merged capstones to multi-step Step*) vs per-operation lower/residue rules. Blocks the echo generalisation to add/eq.",
-]
+issues = []
 
 [critical-next-actions]
 actions = [
-  "Resolve the echo value-shape design fork (A vs B), then add the product type",
-  "TG-1: let-binding type safety via de Bruijn substitution",
-  "Generalise echo to add/eq; thread residue into TangleIR with the quandledb session",
-  "Extend the OCaml typechecker (typecheck.ml/ast.ml) with echo types",
+  "TG-1: let-binding type safety via de Bruijn substitution (Lean 4; ~150 LoC per PROOF-NARRATIVE §TG-1)",
+  "TG-3: formal refinement proof — OCaml typecheck.ml vs Lean HasType",
+  "TangleIR: thread echo residue into TangleIR schema; coordinate with quandledb session",
 ]
 
 [maintenance-status]
-last-run-utc = "2026-06-05T00:00:00Z"
+last-run-utc = "2026-06-14T03:00:00Z"
 last-result = "pass"               # unknown | pass | warn | fail
-notes = "lean-proofs oracle GREEN (PR #34, #36 merged); Tangle.lean 0 errors, no sorry/axiom/admit"
+notes = "dune build + dune test (548/548) GREEN after PR #46; lean-proofs CI GREEN; Tangle.lean 26 HasType rules / 57 Step rules, 0 errors, no sorry/axiom/admit"

.machine_readable/bot_directives/tangle.directives.a2ml

@@ -4,7 +4,7 @@
 # tangle.directives.a2ml — directives for the bot fleet on hyperpolymath/tangle
 [metadata]
 version = "1.0.0"
-last-updated = "2026-06-05"
+last-updated = "2026-06-14"
 applies-to = ["hypatia", "gitbot-fleet", "git-private-farm"]
 
 [development]

CHANGELOG.md

@@ -13,7 +13,17 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
 ## [Unreleased]
 
+### Echo types OCaml pipeline (PR #45 + #46)
+
 ### Added
+- Echo/product type system fully landed in the OCaml pipeline (PR #45 + #46):
+  - `ast.ml`: 8 new `expr` constructors (`echoClose`, `lower`, `residue`, `pair`, `fst`, `snd`, `echoAdd`, `echoEq`); 2 new `ty` constructors (`TProd`, `TEcho`)
+  - `typecheck.ml`: 8 new `infer_expr` rules mirroring Lean `HasType` (`T-Echo-Close`, `T-Lower`, `T-Residue`, `T-Pair`, `T-Fst`, `T-Snd`, `T-Echo-Add`, `T-Echo-Eq`); `pp_ty` made `rec`
+  - `eval.ml`: `VEcho`/`VPair` value forms; 8 new `eval_expr` arms; `pp_value` made `rec`
+  - `lexer.mll` + `parser.mly` + `token.ml`: keyword tokens and grammar productions for all 8 surface forms (`echoClose(e)`, `lower(e)`, `residue(e)`, `pair(a,b)`, `fst(e)`, `snd(e)`, `echoAdd(a,b)`, `echoEq(a,b)`)
+  - `pretty.ml`: pretty-printers for all 8 forms; round-trips through parser
+- TG-4 (pretty-print/parse round-trip) discharged: `test_roundtrip.ml` extended with 16 new TG-4 entries covering every echo/product constructor (PR #46)
+- `docs/spec/ECHO-TANGLEIR-THREADING.md`: cross-repo contract for how echo residue threads through TangleIR to QuandleDB (PR #45)
 - Compositional PD compiler API (`compositional.ml` / `.mli`):
   `expr`, `planar_diagram`, `compiled`, `skein_payload` types
 - `pdv1_blob_of_pd`: canonical text serialisation format
@@ -29,6 +39,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 - Zig ABI layer modernized
 
 ### Fixed
+- `compiler/bin/main.ml` debug token printer: add 8 missing echo keyword token arms (Warning 8 exhaustiveness, PR #46)
+- `compiler/lib/typecheck.ml` `strand_type_of_ty`: add `TProd`/`TEcho` arms (Warning 8 exhaustiveness, PR #46)
 - EXPLAINME.adoc section heading quotes
 
 ## Earlier commits (no versions tagged)

PROOF-NARRATIVE.md

@@ -31,7 +31,7 @@ Tangle is the **semantic core** of a four-layer federated stack:
                   ▼
 ┌─────────────────────────────────────────────────────────┐
 │  Tangle CORE  (THIS REPO)                               │
-│    proofs/Tangle.lean — 16 mechanised results           │
+│    proofs/Tangle.lean — mechanised results (26 HasType, 57 Step) │
 │    compiler/lib/*.ml — OCaml implementation             │
 │    compiler/tangle-wasm — WASM backend                  │
 │    compiler/tangle-lsp — LSP server                     │
@@ -51,8 +51,8 @@ delivered slice and the remaining gap explicit.
 
 ## 2. Proven now
 
-All 16 results live in [`proofs/Tangle.lean`](proofs/Tangle.lean)
-(Lean 4, ~570 LoC, no `sorry`, no `axiom`).
+All results live in [`proofs/Tangle.lean`](proofs/Tangle.lean)
+(Lean 4, no `sorry`, no `axiom`).
 
 **Build oracle.** As of 2026-06-01 (PR closing TG-0, hyperpolymath/tangle#32),
 the file is verified at every push/PR by `.github/workflows/lean-proofs.yml`,
@@ -116,11 +116,13 @@ themselves proofs of the form "these are the rules"):
 - **`Expr`** — the AST (mirrors `compiler/lib/ast.ml`)
 - **`Ty`** — `num`, `str`, `bool`, `word n`
 - **`IsValue`** — value predicate
-- **`HasType`** — typing judgment, 16 rules (`tNum`, `tStr`, `tBool`,
+- **`HasType`** — typing judgment, 26 rules: 13 base (`tNum`, `tStr`, `tBool`,
   `tIdentity`, `tBraid`, `tComposeWord`, `tTensorWord`, `tPipeline`,
-  `tCloseWord`, `tAddNum`, `tEqWord`, `tEqNum`, `tEqStr`, plus the echo
-  rules `tEchoClose`, `tLower`, `tResidue`)
-- **`Step`** — small-step semantics, 31 rules (26 base + 5 echo)
+  `tCloseWord`, `tAddNum`, `tEqWord`, `tEqNum`, `tEqStr`); 4 echo-close
+  (`tEchoClose`, `tLower`, `tResidue`, `tEchoVal`); 7 product+echo-binary
+  (`tPair`, `tFst`, `tSnd`, `tEchoAdd`, `tEchoEqWord`, `tEchoEqNum`,
+  `tEchoEqStr`); 2 let/var (`tVar`, `tLet`)
+- **`Step`** — small-step semantics, 57 rules: 27 base, 9 echo-close/lower/residue, 6 product, 11 echoAdd/echoEq, 2 let, 2 StepStar
 
 These are the formal spec the OCaml implementation is meant to refine
 (see TG-3 below).
@@ -145,6 +147,11 @@ type system*.
 | `echoClose e` | `Word[n] → Echo (Word[n]) (Word[0])` | `echo-intro close` |
 | `lower e` | `Echo ρ τ → τ` — project to result (forget residue) | the collapse / `proj₂` |
 | `residue e` | `Echo ρ τ → ρ` — recover the witness braid | `proj₁` |
+| `pair(a, b)` | `α → β → α × β` — product introduction | `Echo.Pair` (product as residue carrier) |
+| `fst(e)` | `α × β → α` — first projection | `proj₁` |
+| `snd(e)` | `α × β → β` — second projection | `proj₂` |
+| `echoAdd(a, b)` | `Num → Num → Echo (Num × Num) Num` — addition with summand residue | `echo-intro add` |
+| `echoEq(a, b)` | `ρ → ρ → Echo (ρ × ρ) Bool` — equality with operand residue | `echo-intro eq` |
 
 **Metatheory.** Progress, Preservation, Determinism, and Type Safety all
 cover `echoClose`/`lower`/`residue` (the inductions are exhaustive over
@@ -167,6 +174,27 @@ its residue `v` is.
 
 Tracked as obligation **TG-10** in PROOF-NEEDS.md (landed).
 
+## 2.6 OCaml implementation completeness
+
+As of 2026-06-14 (PRs #45–#46), the OCaml pipeline (`compiler/lib/`) covers the
+complete echo + product fragment described in §2.5:
+
+| Layer | Echo/product coverage |
+|-------|-----------------------|
+| `ast.ml` | `EchoClose`, `Lower`, `Residue`, `Pair`, `Fst`, `Snd`, `EchoAdd`, `EchoEq` in `expr`; `TProd`, `TEcho` in `ty` |
+| `typecheck.ml` | 8 `infer_expr` rules matching Lean `HasType`; `pp_ty` made `rec` |
+| `eval.ml` | `VEcho`, `VPair` values; 8 `eval_expr` arms; `pp_value` made `rec` |
+| `lexer.mll` / `parser.mly` / `token.ml` | Keyword tokens + grammar productions for all 8 surface forms |
+| `pretty.ml` | Pretty-printers for all 8 forms |
+| `test_roundtrip.ml` | TG-4 round-trip property test: 36 entries including all 8 echo/product constructors |
+
+**Build oracle**: `dune build` + `dune test` (548/548) green since PR #46. The
+pre-PR #46 `main` did not compile due to two `Warning 8` exhaustiveness gaps
+(both fixed: `strand_type_of_ty` in `typecheck.ml`; debug token printer in `bin/main.ml`).
+
+**TG-3 gap remains**: the OCaml typechecker is not yet proven to refine `HasType`;
+the correspondence is validated by the test suite, not by a formal translation.
+
 ## 3. Remaining obligations (the narrative arc)
 
 What's not yet proven, why it matters, and what assumption each rests on.
@@ -234,6 +262,9 @@ claim is unchecked.
 
 ### TG-4 — Pretty-print/parse round-trip
 
+**Status: LANDED** (PR #46). `compiler/test/test_roundtrip.ml` extended with
+36 entries including all 8 echo/product constructors; 548/548 tests pass.
+
 **Claim.** `parse(pretty e) = e` for every closed value `e`.
 
 **Why valuable.** Free fuzz oracle. Also the foundation of any "IR
@@ -245,7 +276,7 @@ viewer" tooling that re-parses what `pretty` emitted.
 - [[A-TG-4.2]] Lexer never strips information needed by the parser
   (e.g. whitespace within braid literals).
 
-**How to discharge.** Property test in `compiler/test/`.
+**How to discharge.** Property test in `compiler/test/` — discharged.
 
 ### TG-5 — `compositional.ml` rewriter preserves types
 

PROOF-NEEDS.md

@@ -40,8 +40,9 @@ and `proofs/Tangle.lean`:
 **Coverage:** the **let-free fragment** of core Tangle, comprising
 `Num`, `Str`, `Bool`, `Identity`, `BraidLit`, `Compose`, `Tensor`,
 `Pipeline`, `Close`, `Add`, `Eq`, plus the **echo-types fragment**
-(`EchoClose`, `Lower`, `Residue` with type former `Echo[ρ,τ]`). 16 typing
-rules, 31 step rules. All four theorems cover the echo fragment (TG-10).
+(`EchoClose`, `Lower`, `Residue`, `EchoAdd`, `EchoEq`) and the **product type**
+(`Pair`, `Fst`, `Snd` with type former `ρ × σ`). 26 typing rules, 57 step rules.
+All four theorems cover the echo fragment (TG-10).
 
 ## What remains
 
@@ -52,13 +53,13 @@ Cross-referenced to [PROOF-NARRATIVE.md §3](PROOF-NARRATIVE.md#3-remaining-obli
 | TG-1 | Extend Progress/Preservation/Determinism/TypeSafety to `let`-binding | TP | Lean 4 | P1 | 3d | NOT STARTED (acknowledged in Tangle.lean header) |
 | TG-2 | Type checking is decidable: define `infer : Expr → Option Ty` proven equivalent to `HasType` | ALG | Lean 4 | P1 | 1d | NOT STARTED |
 | TG-3 | OCaml `typecheck.ml` refines the Lean `HasType` spec | TP | Lean 4 + translation validation | P1 | 5d | NOT STARTED |
-| TG-4 | Pretty-print/parse round-trip on closed values | INV | OCaml property test (cheap) | P2 | 4h | NOT STARTED |
+| TG-4 | Pretty-print/parse round-trip on closed values | INV | OCaml property test (cheap) | P2 | 4h | **LANDED** (PR #46 — OCaml property test in `compiler/test/test_roundtrip.ml`, 36 entries including 16 echo/product forms) |
 | TG-5 | `compositional.ml` (418 LoC) rewriter preserves types | TP | Lean 4 + OCaml test file | P2 | 3d | NOT STARTED (B6: no test file yet) |
 | TG-6 | WASM compilation preserves semantics (source eval ≡ wasm exec) | TP / ALG | Lean 4 bisimulation | P1 | 3w (research-grade) | NOT STARTED |
 | TG-7 | `Step.eqBraids` decides braid-group equivalence (not list equality) | ALG / DOM | OCaml + Lean 4 | P2 | 2w | NOT STARTED (current impl is soundness-floor, not completeness) |
 | TG-8 | Each dialect (braid-calculus, quantum-circuit, skein-algebra, string-diagram, virtual-knot) is a conservative extension of core | TP | Lean 4 per-dialect | P3 | 1w each | NOT STARTED |
 | TG-9 | LSP diagnostics are a subset of `HasType` failures (no LSP-only diagnostics) | INV | Audit + refactor | P2 | 1d | NOT STARTED |
-| TG-10 | Echo-types integrated into the type system: `Echo[ρ,τ]` former + `echoClose`/`lower`/`residue`, with Progress/Preservation/Determinism/TypeSafety extended to cover them and the non-injectivity / residue-recovery capstones proven | TP / DOM | Lean 4 | P1 | — | **LANDED** (`proofs/Tangle.lean` §ECHO-TYPES) |
+| TG-10 | Echo-types integrated into the type system: `Echo[ρ,τ]` former + `echoClose`/`lower`/`residue`/`echoAdd`/`echoEq` + product type (`pair`/`fst`/`snd`), with Progress/Preservation/Determinism/TypeSafety extended to cover them and the non-injectivity / residue-recovery capstones proven | TP / DOM | Lean 4 | P1 | — | **LANDED** (`proofs/Tangle.lean` §ECHO-TYPES) |
 
 For full per-obligation statements, _why valuable_, and the
 assumptions each rests on, see PROOF-NARRATIVE.md.

docs/echo-types-ocaml-pipeline.md

@@ -0,0 +1,156 @@
+<!--
+SPDX-License-Identifier: MPL-2.0
+Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+-->
+# Echo Types — OCaml Pipeline Integration
+
+> **Status**: Complete (PRs #45, #46, merged 2026-06-14).
+> This page is the developer reference for the echo/product type integration
+> in the OCaml compiler pipeline. For the formal metatheory see
+> [PROOF-NARRATIVE.md §2.5](../PROOF-NARRATIVE.md) and
+> [`proofs/Tangle.lean` §ECHO-TYPES](../proofs/Tangle.lean).
+> For the cross-repo contract with QuandleDB see
+> [ECHO-TANGLEIR-THREADING.md](spec/ECHO-TANGLEIR-THREADING.md).
+
+---
+
+## 1. What are echo types?
+
+Echo types make structured loss **recoverable at the type level**. Tangle's
+canonical lossy operation is `close : Word[n] → Word[0]`, which collapses any
+braid to the identity, discarding the word. An `Echo ρ τ` value is a pair:
+
+- **result** (`τ`) — what the lossy operation produces
+- **residue** (`ρ`) — the pre-closure braid, retained in the type
+
+The design mirrors `Echo f y := Σ (x : A), f x ≡ y` from
+`hyperpolymath/echo-types` (`Echo.agda`) in Tangle's simply-typed setting.
+
+The **product type** `ρ × σ` serves as the residue carrier for binary lossy
+operations: `echoAdd` keeps both summands, `echoEq` keeps both operands.
+
+---
+
+## 2. Surface syntax
+
+| Expression | Type | Meaning |
+|------------|------|---------|
+| `echoClose(e)` | `Word[n] → Echo (Word[n]) (Word[0])` | Close a braid, retaining the original as residue |
+| `lower(e)` | `Echo ρ τ → τ` | Project to the result (forget the residue) |
+| `residue(e)` | `Echo ρ τ → ρ` | Recover the witness braid |
+| `pair(a, b)` | `α → β → α × β` | Construct a product |
+| `fst(e)` | `α × β → α` | First projection |
+| `snd(e)` | `α × β → β` | Second projection |
+| `echoAdd(a, b)` | `Num → Num → Echo (Num × Num) Num` | Addition retaining summand pair as residue |
+| `echoEq(a, b)` | `ρ → ρ → Echo (ρ × ρ) Bool` | Equality retaining operand pair as residue |
+
+---
+
+## 3. OCaml pipeline layers
+
+### 3.1 AST (`compiler/lib/ast.ml`)
+
+```ocaml
+type expr =
+  ...
+  | EchoClose of expr
+  | Lower     of expr
+  | Residue   of expr
+  | Pair      of expr * expr
+  | Fst       of expr
+  | Snd       of expr
+  | EchoAdd   of expr * expr
+  | EchoEq    of expr * expr
+
+type ty =
+  ...
+  | TProd of ty * ty    (* ρ × σ — product residue carrier *)
+  | TEcho of ty * ty    (* Echo ρ τ *)
+```
+
+### 3.2 Typechecker (`compiler/lib/typecheck.ml`)
+
+Eight new `infer_expr` cases, all mirroring Lean `HasType`:
+
+| OCaml rule | Lean rule | Type produced |
+|-----------|-----------|--------------|
+| `EchoClose e` | `tEchoClose` | `TEcho (TEcho(Word[n], inferred_width), TWord 0)` → simplified to `TEcho(ρ, TWord 0)` |
+| `Lower e` | `tLower` | `τ` (from `TEcho ρ τ`) |
+| `Residue e` | `tResidue` | `ρ` (from `TEcho ρ τ`) |
+| `Pair(a, b)` | `tPair` | `TProd(α, β)` |
+| `Fst e` | `tFst` | `α` (from `TProd α β`) |
+| `Snd e` | `tSnd` | `β` (from `TProd α β`) |
+| `EchoAdd(a, b)` | `tEchoAdd` | `TEcho(TProd(TNum, TNum), TNum)` |
+| `EchoEq(a, b)` | `tEchoEqWord/Num/Str` | `TEcho(TProd(ρ, ρ), TBool)` |
+
+### 3.3 Evaluator (`compiler/lib/eval.ml`)
+
+New value forms:
+
+```ocaml
+type value =
+  ...
+  | VEcho of value * value   (* (residue, result) — Option B uniform form *)
+  | VPair of value * value   (* product value *)
+```
+
+Echo values use the **Option B** uniform shape: `VEcho(residue, result)` in all
+cases. `echoClose` produces `VEcho(braid_value, VIdentity)`. `echoAdd` produces
+`VEcho(VPair(n1, n2), VNum(n1 + n2))`. `echoEq` produces `VEcho(VPair(v1, v2),
+VBool(v1 = v2))`.
+
+### 3.4 Lexer / parser / tokens
+
+Tokens (`compiler/lib/token.ml`):
+`ECHOCLOSE`, `LOWER`, `RESIDUE`, `PAIR`, `FST`, `SND`, `ECHOADD`, `ECHOEQ`
+
+All 8 keywords are registered in the lexer (`lexer.mll`) and have dedicated
+grammar productions in `parser.mly` following the existing unary
+(`KW LPAREN expr RPAREN`) and binary (`KW LPAREN expr COMMA expr RPAREN`) patterns.
+
+### 3.5 Pretty printer (`compiler/lib/pretty.ml`)
+
+All 8 forms pretty-print to the same surface syntax that the parser accepts,
+satisfying the TG-4 round-trip obligation.
+
+---
+
+## 4. Round-trip guarantee (TG-4)
+
+`compiler/test/test_roundtrip.ml` tests `parse(pretty(e)) = e` and
+`pretty(parse(pretty(parse(s)))) = pretty(parse(s))` for every constructor.
+
+Echo/product entries:
+`echoClose`, `lower`, `residue`, `pair`, `fst`, `snd`, `echoAdd`, `echoEq`
+— 16 test cases (8 basic + 8 idempotent), all passing as of PR #46.
+
+---
+
+## 5. Proof coverage
+
+The formal spec (`proofs/Tangle.lean`) covers the complete echo+product fragment:
+
+| Lean theorem | Coverage |
+|-------------|----------|
+| `T-Progress` | All 8 echo/product expression forms |
+| `T-Preservation` | All 8 echo/product expression forms |
+| `T-Determinism` | All 8 echo/product expression forms |
+| `T-TypeSafety` | Corollary (progress + preservation) |
+| `echo_lower_collapses` | Every closed braid lowers to `identity` |
+| `echo_residue_recovers` | `residue(echoClose(braid[gs])) →* braid[gs]` |
+| `echo_distinguishes_collapsed` | Distinct braids keep distinct residues after `lower` |
+| `echo_roundtrip_typed` | Round-trip is well-typed |
+
+The OCaml typechecker is not yet formally proven to refine `HasType` (TG-3,
+open). Correspondence is validated by the test suite (548/548 passing).
+
+---
+
+## 6. Known gaps and future work
+
+| Gap | Tracking |
+|-----|----------|
+| TG-3: formal OCaml–Lean refinement proof | PROOF-NEEDS.md TG-3 |
+| TG-1: type safety extended to `let` | PROOF-NEEDS.md TG-1 |
+| TangleIR: thread echo residue into schema | ECHO-TANGLEIR-THREADING.md |
+| `echoClose` in WASM backend | tangle-wasm (not yet implemented) |