diff --git a/README.md b/README.md
index a4ba4e4..e4e53ef 100644
--- a/README.md
+++ b/README.md
@@ -1,78 +1,95 @@
 # Stellogen
 
-**Note: this project is an experimental proof of concept, not a fully
-designed or specified programming language. It is better understood as a
-research project or an esoteric language.**
+Stellogen is an experimental, "logic agnostic" language that asks: what if
+programs and their meaning were built from the same raw material, term
+unification, without types or logic imposed from above?
 
 Stellogen is a *logic-agnostic* programming language based on term unification.
 It has been designed from concepts of Girard's transcendental syntax.
 
+Stellogen explores a different way of thinking about programming languages:
+instead of relying on primitive types or fixed logical rules, it is built on
+the simple principle of term unification. The goal is not to replace existing
+languages, but to test how far this idea can be pushed and what new programming
+paradigms might emerge from it.
+
+**For the moment, it is an experimental proof of concept, not a fully
+designed or specified programming language. It is better understood as a
+research project or an esoteric language.**
+
+## Philosophy
+
+Programs exist to solve needs, but they don’t always behave as expected. To
+reduce this gap, we use a separate formal language of types. Types act like
+**questions** we can ask, and programs act as **answers**.
+
+This language of types is powerful, but it also shapes and constrains the way
+we design programs. It defines which questions are even possible to ask. Typed
+functional languages, dependent types, and other formal systems provide
+remarkable guarantees, but they also impose a logic you must follow, even when
+you might prefer to proceed more directly, or even outside of such a system.
+
+Stellogen takes another path. It offers elementary interactive building blocks
+where both computation and meaning live in the same language. In this setting,
+compilers and interpreters no longer carry semantic authority: their role is
+only to check that blocks connect. The semantic power (and the responsibility
+that comes with it) belongs entirely to the user.
+
 ## Key characteristics
 
-- **typable** but without primitive types nor type systems
-- both computation and typing are based on basic **term unification** between
-blocks of terms.
+- Programs are **typable**, but without primitive types or predefined type
+systems;
+- Both computation and typing rely on the same mechanism: **term unification**.
+- It is multi-paradigm:
 
-It is multi-paradigm:
-- _logic programs_ called "constellations" are the elementary blocks of
-programming;
-- _functional programs_ correspond to layered constellations enforcing an order
-of interaction;
-- _imperative programs_ are iterative recipes constructing constellations;
-- _objects_ are ways to structure constellations.
+| Paradigm        | Stellogen equivalent                                     |
+| --------------- | ---------------------------------------------------------|
+| Logic           | Constellations (elementary blocks)                       |
+| Functional      | Layered constellations enforcing order of interaction    |
+| Imperative      | Iterative recipes for building constellations            |
+| Object-oriented | Structured constellations                                |
 
 ## Influences
 
-It draws (or try to draw) inspiration from:
-- Prolog/Datalog (for unification-based computation and constraint solving);
-- Smalltalk (for message-passing, object-oriented paradigm and minimalism);
-- Coq (for proof-as-program paradigm and iterative programming with tactics);
-- Scheme/Racket (for minimalism and metaprogramming);
-- Shen (for its optional type systems and its "power and responsibility"
-philosophy).
+Stellogen borrows ideas from several traditions: from **Prolog/Datalog** for
+the power of unification; from **Smalltalk** for the minimalism of
+message-passing and objects; from **Rocq** for the proof-as-program paradigm;
+from **Scheme/Racket** for the spirit of metaprogramming; and from **Shen** for
+the philosophy of optional type systems where *power comes with responsibility*.
+
+## How it works
 
-## Syntax samples
+The language uses extended S-expressions.
 
-Finite state machine
+Here is a commented example of the definition of a finite state machine
+accepting words ending with `00`.
 
 ```
+' We define a macro 'spec' for type definition
+' It is just an alias for the definition [:=]
 (new-declaration (spec X Y) (:= X Y))
+
+' We define a macro for type assertion
 (new-declaration (:: Tested Test)
-  (== @(interact @#Tested #Test) ok))
+  (== @(interact @#Tested #Test) ok)) ' triggers interaction and expects [ok]
 
+' The type [binary] is defined as a set of three interactive tests
+' According to the previous macro, the tests pass when interaction gives [ok]
 (spec binary {
-  [(-i []) ok]
-  [(-i [0|X]) (+i X)]
-  [(-i [1|X]) (+i X)]})
-
-'input words
-(:= e (+i []))        (:: e binary)
-(:= 0 (+i [0]))       (:: 0 binary)
-(:= 000 (+i [0 0 0])) (:: 000 binary)
-(:= 010 (+i [0 1 0])) (:: 010 binary)
-(:= 110 (+i [1 1 0])) (:: 110 binary)
-
-'''
-automaton accepting words ending with 00
-'''
-(:= (initial Q) [(-i W) (+a W Q)])
-(:= (accept Q) [(-a [] Q) accept])
-(:= (if read C1 on Q1 then Q2) [(-a [C1|W] Q1) (+a W Q2)])
-
-(:= a1 {
-  #(initial q0)
-  #(accept q2)
-  #(if read 0 on q0 then q0)
-  #(if read 0 on q0 then q1)
-  #(if read 1 on q0 then q0)
-  #(if read 0 on q1 then q2)})
-
-(:= kill (-a _ _))
-
-(show (process (interact @#e #a1)   #kill))
-(show (process (interact @#000 #a1) #kill))
-(show (process (interact @#010 #a1) #kill))
-(show (process (interact @#110 #a1) #kill))
+  [(-i []) ok]          ' returns [ok] on empty list
+  [(-i [0|X]) (+i X)]   ' matches on [0] and checks the tail
+  [(-i [1|X]) (+i X)]}) ' matches on [1] and checks the tail
+                        ' otherwise the term remains unchanged
+
+' We define some words
+(:= word1 (+i [0 1 1]))
+(:= word2 (+i [2 3]))
+
+' succeeds -> [ok] is obtained on interaction with test [binary]
+(:: word1 binary)
+
+' fails
+' (:: word2 binary)
 ```
 
 More examples can be found in `examples/`.
@@ -83,8 +100,10 @@ This project is still in development, hence the syntax and features
 are still changing frequently.
 
 To learn more about the current implementation of stellogen:
-- French guide (official): https://tsguide.refl.fr/
-- English guide: https://tsguide.refl.fr/en/
+
+https://github.com/engboris/stellogen/wiki/Basics-of-Stellogen
+
+A more complete guide is in production.
 
 # Use
 
diff --git a/guide/en/.gitignore b/guide/en/.gitignore
deleted file mode 100644
index 7585238..0000000
--- a/guide/en/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-book
diff --git a/guide/en/Makefile b/guide/en/Makefile
deleted file mode 100644
index 2759ca7..0000000
--- a/guide/en/Makefile
+++ /dev/null
@@ -1,7 +0,0 @@
-all:
-	deploy
-
-deploy:
-	git pull
-	mdbook build
-	sudo rsync -aux book/. /var/www/tsguide.refl.fr/en/.
diff --git a/guide/en/book.toml b/guide/en/book.toml
deleted file mode 100644
index f401c04..0000000
--- a/guide/en/book.toml
+++ /dev/null
@@ -1,6 +0,0 @@
-[book]
-authors = ["engboris"]
-language = "en"
-multilingual = false
-src = "src"
-title = "tsguide"
diff --git a/guide/en/src/SUMMARY.md b/guide/en/src/SUMMARY.md
deleted file mode 100644
index 1e86418..0000000
--- a/guide/en/src/SUMMARY.md
+++ /dev/null
@@ -1,48 +0,0 @@
-# Summary
-
-# Context
-
-- [Introduction](./introduction/introduction.md)
-- [Philosophy](./introduction/philosophy.md)
-- [Getting started](./introduction/start.md)
-
-# Constellations and their execution
-
-- [Term unification](./stellarresolution/unification.md)
-- [Stars and constellations](./stellarresolution/entities.md)
-- [Execution of constellations](./stellarresolution/execution.md)
-
-# Basics of Stellogen
-
-- [Defining constellations](./stellogen/definitions.md)
-- [Commands](./stellogen/commands.md)
-- [Reactive effects](./stellogen/effects.md)
-- [Substitutions](./stellogen/substitutions.md)
-- [Logic programming](./stellogen/prolog.md)
-
-# Object-oriented programming
-
-- [Galaxies](./objects/galaxies.md)
-- [Interfaces](./objects/interfaces.md)
-
-# Typing
-
-- [Specficiations](./typing/spec.md)
-- [Expectations](./typing/expect.md)
-
-# Imperative programming
-
-- [Processes](./imperative/processes.md)
-
-# State machines
-
-- [Finite automata (TODO)](./automata/nfsa.md)
-- [Transducers (TODO)](./automata/transducers.md)
-- [Pushdown automata (TODO)](./automata/pda.md)
-- [Turing machines (TODO)](./automata/turing.md)
-
-# Functional programming
-
-- [Untyped linear lambda-calculus (TODO)](./lambda/untypedlin.md)
-- [Linear types (TODO)](./lambda/lintypes.md)
-- [Simply typed lambda-calculus (TODO)](./lambda/stlc.md)
diff --git a/guide/en/src/imperative/processes.md b/guide/en/src/imperative/processes.md
deleted file mode 100644
index b85bd53..0000000
--- a/guide/en/src/imperative/processes.md
+++ /dev/null
@@ -1,70 +0,0 @@
-## Construction process
-
-We can chain constellations with the expression `process ... end`:
-
-```
-c = process
-  +n0(0).
-  -n0(X) +n1(s(X)).
-  -n1(X) +n2(s(X)).
-end
-```
-
-This chain starts with the first constellation `+n0(0)` as a state space. The
-next constellation then interacts as an action space with the previous one 
-seen as a state space). Thus we
-have an interaction chain with a complete focus on the previous result.
-
-It's as if we did the following computation:
-
-```
-c = +n0(0).
-c = @#c {-n0(X) +n1(s(X))}.
-c = @#c {-n1(X) +n2(s(X))}.
-```
-
-> This is what corresponds to tactics in proof assistants such as Coq and could
-be assimilated to imperative programs which alter state representations
-(memory, for example).
-
-> Dynamical constructions correspond to the notion of "proof-process" in Boris
-Eng or "proof-trace" in Pablo Donato. Proof-processes construct proof-objects
-(constellations).
-
-## Process termination
-
-In the result of an execution, if we represent results as rays with zero
-polarity, then stars containing polarized rays can be interpreted as
-incomplete computations that could be discarded.
-
-To achieve this in construction processes, we can use the special `#kill`
-expression:
-
-```
-c = process
-  +n0(0).
-  -n0(X) +n1(s(X)).
-  -n1(X) +n2(s(X)).
-  -n2(X) result(X); -n2(X) +n3(X).
-  #kill.
-end
-
-show-exec c.
-```
-
-We used a ray `+n3(X)` to continue computations if desired. The result is stored in `result(X)`.
-However, if we want to keep only the result and eliminate any further
-computation possibilities, we can use `#kill`.
-
-## Process Cleanup
-
-Sometimes we encounter empty stars `[]` in processes. These can be removed
-using the `#clean` command:
-
-```
-show-exec process
-  +f(0).
-  -f(X).
-  #clean.
-end
-```
diff --git a/guide/en/src/introduction/introduction.md b/guide/en/src/introduction/introduction.md
deleted file mode 100644
index 385392d..0000000
--- a/guide/en/src/introduction/introduction.md
+++ /dev/null
@@ -1,39 +0,0 @@
-# Introduction
-
-Welcome to the guide to the Stellogen language.
-
-**Please note that this guide is highly experimental and subject to frequent
-changes. The language it describes is equally unstable.**
-
-I welcome any opinions, recommendations, suggestions, or simple
-questions. Feel free to contact me at
-[boris.eng@proton.me](mailto:boris.eng@proton.me).
-
-Happy reading!
-
-Translated from the French guide by:
-- noncanonicAleae
-- ChatGPT 4o
-
-## How it all began
-
-Stellogen was created from Boris Eng's research to understand Jean-Yves
-Girard's transcendent syntax program.
-
-Transcendent syntax proposes a new foundation for logic and computation,
-extending the Curry-Howard correspondence. In this new framework, logical
-entities such as proofs, formulas, and concepts like truth are redefined/built
-from an elementary computational model called "stellar resolution," which is a
-highly flexible form of logical programming language.
-
-To experiment with these ideas, Eng developed an interpreter called the "Large
-Star Collider (LSC)" to execute stellar resolution expressions. It was
-initially developed in Haskell and later reimplemented in OCaml.
-
-Later, it became apparent that a metaprogramming language was necessary to
-properly work with these objects, especially for writing proofs in linear
-logic (which was the original project). This led to the creation of the
-Stellogen language.
-
-Over time, Stellogen gradually diverged from transcendent syntax to develop
-its own concepts.
diff --git a/guide/en/src/introduction/philosophy.md b/guide/en/src/introduction/philosophy.md
deleted file mode 100644
index f9f61cb..0000000
--- a/guide/en/src/introduction/philosophy.md
+++ /dev/null
@@ -1,71 +0,0 @@
-# Philosophy
-
-## Mechanics of meaning
-
-Types, specifications, algorithms, and logical formulas are **questions** that
-we pose. They carry a subjective *intention*. Programs are **answers** to
-these questions. They follow an objective dynamic: they can be implicit and
-evolve into an irreducible explicit form (this is execution leading to a
-computational result).
-
-The big question is: how can we determine whether we are facing an answer to a question? We need a connective framework for the interaction between questions and answers.
-
-## Iconoclasm and decentralization
-
-Traditionally, logic and type systems define systems with:
-- classes of entities (first-order individuals and relations);
-- semantic rules (the compiler/interpreter is responsible for the meaning of
-expressions, and the user manipulates these expressions according to this meaning);
-- forbidden interactions;
-- allowed interactions.
-
-This establishes a preconceived logical framework. In particular, compilers and
-interpreters hold semantic authority: they define which questions can be asked
-and how to judge whether an answer is valid.
-
-Stellogen seeks to return semantic power to the user, making them responsible
-for creating meaning through elementary building blocks that compose both
-programs and types/formulas/specifications. Interpreters and compilers then
-take on the role of maintaining a basic core that ensures proper connectivity
-between these blocks, as well as managing metaprogramming. This shifts their
-role from semantic authority to protocol and administrative evaluation.
-
-## Meaning through experience
-
-To determine whether a program has a certain type (if an answer satisfies a
-question), we proceed as follows:
-- we construct a type by defining a set of tests that must be passed—these
-tests are themselves programs;
-- we build a "judge" that determines what it means to "pass a test";
-- we connect a program to each test of the type and check whether the judge
-validates all interactions.
-
-This provides non-systemic, local guarantees, similar to "assert" statements in
-programming. We could choose to organize types and constraints within
-structured systems if needed.
-
-## Order in chaos
-
-The computational model we work with, based on elementary building blocks,
-could be described as chaotic. It is possible to write unintuitive constructs
-with unpredictable outcomes. In some cases, confluence does not even hold 
-different execution orders lead to different results).
-
-There are two ways to bring order to chaos:
-- natural, local emergence by creating local guarantees on program fragments;
-- imposing a closed system that defines restrictions/constraints in which only
-certain types can be used.
-
-Stellogen aims to leave both possibilities open. The first choice allows for
-great flexibility, while the second provides efficiency and usability
-advantages, along with stronger guarantees.
-
-## Partial verification
-
-From a programming perspective, particularly in formal methods, Stellogen is
-driven by a notion of "partial" verification, in contrast to total
-verification, where a program and its properties are fully modeled to obtain
-formal proofs.
-
-Stellogen focuses on expressive local constraints that could later be
-integrated into a broader system.
diff --git a/guide/en/src/introduction/start.md b/guide/en/src/introduction/start.md
deleted file mode 100644
index 15d02e6..0000000
--- a/guide/en/src/introduction/start.md
+++ /dev/null
@@ -1,18 +0,0 @@
-# Getting started
-
-To install the Stellogen interpreter, go to this Git repository:
-
-[https://github.com/engboris/stellogen](https://github.com/engboris/stellogen)
-
-You can either compile from [sources](https://github.com/engboris/stellogen/blob/master/README.md#build-from-sources) or download a pre-compiled executable:
-
-- For Linux x86-x64: [https://github.com/engboris/stellogen/releases](https://github.com/engboris/stellogen/releases)
-
-You can then simply write your programs in any text file and follow the instructions in the [README.md](https://github.com/engboris/stellogen/blob/master/README.md#commands) file of the git repository to execute your programs.
-
-For a quick preview, don't hesitate to look up:
-
- - [syntactic reference (cheat sheet)](https://github.com/engboris/stellogen/blob/master/examples/syntax.sg);
- - [program examples](https://github.com/engboris/stellogen/tree/master/examples);
-
-If you are ready, let's go!
diff --git a/guide/en/src/objects/galaxies.md b/guide/en/src/objects/galaxies.md
deleted file mode 100644
index 1147e28..0000000
--- a/guide/en/src/objects/galaxies.md
+++ /dev/null
@@ -1,25 +0,0 @@
-# Galaxies
-
-Constellations can be represented by labelling sub-constellations.
-This is what we call *galaxies*.
-
-Galaxies are defined with blocks `galaxy ... end` containing a series of labels
-`label =` followed by the associated galaxy:
-
-```
-g = galaxy
-  test1 = +f(a) ok.
-  test2 = +f(b) ok.
-end
-```
-
-Fields of a galaxy are then accessed with `->`:
-
-```
-show #g->test1.
-show #g->test2.
-```
-
-> This resembles the concept of a record in programming, except that when
-> galaxies are used, they are represented by their underlying constellation (by
-> forgetting the labels).
diff --git a/guide/en/src/stellarresolution/entities.md b/guide/en/src/stellarresolution/entities.md
deleted file mode 100644
index 2bb3d25..0000000
--- a/guide/en/src/stellarresolution/entities.md
+++ /dev/null
@@ -1,88 +0,0 @@
-# Stars and Constellations
-
-## Rays
-
-The language of stellar resolution extends the notion of terms with the concept
-of *rays*. A ray is a term where function symbols are polarized with:
-
-- `+` (positive polarity);
-- `-` (negative polarity);
-- nothing (neutral polarity or absence of polarity).
-
-The *compatibility* of rays follows the same rules as term unification,
-except:
-- instead of requiring equality `f = g` of function symbols when
-`f(t1, ..., tn)` is confronted with `g(u1, ..., un)`, we require `f` and `g` to have opposite polarities (`+` versus `-`);
-symbols without polarity cannot interact.
-
-For example:
-- `+f(X)` and `-f(h(a))` are compatible with `{X:=h(a)}`;
-- `f(X)` and `f(h(a))` are incompatible;
-- `+f(X)` and `+f(h(a))` are incompatible;
-- `+f(+h(X))` and `-f(-h(a))` are compatible with `{X:=a}`;
-- `+f(+h(X))` and `-f(-h(+a))` are compatible with `{X:=+a}`.
-
-### String literals
-
-Stellogen also allows to define special constants representing string literals:
-
-```
-"this is a string literal"
-```
-
-### Sequences
-
-It is possible to use a special infix symbol `:` as in:
-
-```
-+w(0:1:0:1:e).
-```
-
-It is possible to put parentheses around it to make the priorit explicit
-(right-associative by default):
-
-```
-+w((0:(1:(0:(1:e))))).
-+w((((0:1):0):1):e).
-```
-
-## Stars
-
-With rays, we can form *stars*. These are unordered collections of rays
-which can be surrounded by brackets:
-
-```
-+f(X) -f(h(a)) +f(+h(X))
-```
-
-```
-[+f(X) -f(h(a)) +f(+h(X))]
-```
-
-The empty star is denoted as `[]`.
-
-## Constellations
-
-*Constellations* are unordered sequences of stars separated by the `;` symbol
-and ending with a `.`:
-
-```
-+f(X) X; +f(+h(X) a f(b)).
-```
-
-They can be surrounded by braces:
-
-```
-{ +f(X) X; +f(+h(X) a f(b)) }.
-```
-
-Variables are local to their stars. This can be made explicit by writing:
-
-```
-+f(X1) X1; +f(+h(X2) a f(b)).
-```
-
-The empty constellation is denoted as `{}`.
-
-Constellations are, in fact, the smallest objects we can manipulate. They are
-the ones that can be executed in the same way programs are executed.
diff --git a/guide/en/src/stellarresolution/execution.md b/guide/en/src/stellarresolution/execution.md
deleted file mode 100644
index 7e24719..0000000
--- a/guide/en/src/stellarresolution/execution.md
+++ /dev/null
@@ -1,204 +0,0 @@
-# Execution of Constellations
-
-## Fusion of Stars
-
-Stars interact with each other using an operation called fusion (which can be
-likened to an interaction protocol) based on the principle of *Robinson's
-resolution rule*.
-
-The fusion of two stars:
-
-```
-r r1 ... rk
-```
-
-and
-
-```
-r' r1' ... rk'
-```
-
-along their rays `r` and `r'` is defined by a new star:
-
-```
-theta(r1) ... theta(rk) theta(r1') ... theta(rk')
-```
-
-where `theta` is the most general substitution induced by `r` and `r'`.
-
-Note that:
-
-- `r` and `r'` are annihilated during the fusion;
-- the two stars merge;
-- the substitution obtained from resolving the conflict between `r` and `r'`
-propagates to the adjacent rays.
-
-> **Example:** The fusion of `X +f(X)` and `-f(a)` makes `+f(X)` and
-`-f(a)` interact, propagating the substitution `{X:=a}` to the remaining
-ray `X`. The result is `X{X:=a}`, i.e., `a`.
-
-> This fusion operation corresponds to the cut rule in first-order logic (also
-linked to the resolution rule). However, the context here is "alogical" (our
-objects carry no logical meaning).
-
-## Execution
-
-Execution is somewhat akin to solving a puzzle or playing darts. You start with
-a constellation made up of several stars. Choose some *initial stars*, then
-create copies of other stars to interact with them through fusion. The process
-continues until no further interactions are possible (saturation). The final
-constellation is the result of the execution.
-
-Formally, the constellation is split into two parts for execution:
-- the *state space*, corresponding to stars which will be targets for
-interaction;
-- the *action space*, corresponding to stars which will interact with stars of
-the state space.
-
-This separation can be represented as follows, with the action space on the
-left and state space on the right, separated by the symbol `|-`:
-
-```
-a1 ... an |- s1 ... sm
-```
-
-Execution proceeds as follows:
-1. Select a ray `r` from a state star `s`;
-2. Find all possible connections with rays `r'` from action stars `s`;
-3. Duplicate `s` on the right for each such ray `r'` found;
-4. Replace each copy of `s` with the fusion of `a` and `s`;
-5. Repeat until no further interactions are possible in the state space.
-stars.
-
-## Focus
-
-State stars are prefixed by `@`:
-
-```
-@+a b; [-c d].
-```
-
-```
-+a b; [@-c d].
-```
-
-## Example
-
-Consider the execution of the following constellation:
-
-```
-@+a(0(1(e)) q0);
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2).
-```
-
-For the example, we surround the selected way between `>>` and `<<`.
-We have the following step:
-
-```
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2);
-@+a(0(1(e)) q0).
-```
-
-And the following separation:
-
-```
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2)
-|-
-+a(0(1(e)) q0)
-```
-
-Select the first ray of the first star:
-
-```
->>-a(e q2)<< accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2)
-|-
-+a(0(1(e)) q0)
-```
-
-It cannot be connected to `+a(0(1(e)) q0)` because its first argument `e` is
-incompatible with `0(1(e))`. However, it can interact with the two next
-stars (but not the last one because of an incompatibility between `q0` and
-`q1`)
-We do a duplication and a fusion between:
-
-```
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
-```
-
-and
-
-```
-+a(0(1(e)) q0)
-```
-
-and obtain the substitution `{W:=1(e)}` then the result:
-
-```
-+a(1(e) q0);
-+a(1(e) q1)
-```
-
-We obtain the following step:
-
-```
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2)
-|-
-+a(1(e) q0);
-+a(1(e) q1)
-```
-
-The second state star `+a(1(e) q1)` cannot interact with an action star.
-However, we can focus on `+a(1(e) q0)`.
-
-```
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2)
-|-
->>+a(1(e) q0)<<;
-+a(1(e) q1)
-```
-
-It can connect to `-a(1(W) q0)` with substitution `{W:=e}`:
-
-```
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2)
-|-
-+a(e q0);
-+a(1(e) q1)
-```
-
-No further interaction is possible.
-The result of execution is then:
-
-```
-+a(e q0);
-+a(1(e) q1)
-```
diff --git a/guide/en/src/stellarresolution/unification.md b/guide/en/src/stellarresolution/unification.md
deleted file mode 100644
index cc6db34..0000000
--- a/guide/en/src/stellarresolution/unification.md
+++ /dev/null
@@ -1,44 +0,0 @@
-# Term Unification
-
-## Syntax
-
-In unification theory, we write terms. These are either:
-
-- variables (starting with an uppercase letter, such as `X`, `Y`, or `Var`);
-- functions in the form `f(t1, ..., tn)` where `f` is a function symbol
-(starting with a lowercase letter or a digit) and the expressions `t1`, ...,
-`tn` are other terms.
-
-All identifiers (whether for variables or function symbols) can include the
-symbols `_` and `?` (but not at the beginning).
-For example : `is_empty?` and `X_1`.
-
-> **Examples of terms.** `X`, `f(X)`, `h(a, X)`, `parent(X)`, `add(X, Y, Z)`.
-
-It is also possible to omit the comma separating a function's arguments when
-its absence causes no ambiguity. For instance, `h(a X)` can be written instead
-of `h(a, X)`.
-
-## Principle
-
-In unification theory, two terms are said to be unifiable when there exists a
-substitution of variables that makes them identical. For example, `f(X)` and
-`f(h(Y))` are unifiable with the substitution `{X:=h(Y)}` replacing `X` with
-`h(Y)`.
-
-The substitutions of interest are the most general ones. We could consider the
-substitution `{X:=h(c(a)); Y:=c(a)}`, which is equally valid but unnecessarily
-specific.
-
-Another way to look at this is to think of it as connecting terms to check if
-they are compatible or "fit" together:
-
-- A variable `X` connects to anything that does not contain `X` as a subterm;
-otherwise, there would be a circular dependency, such as between `X` and `f(X)`;
-- A function `f(t1, ..., tn)` is compatible with `f(u1, ..., un)` where `ti` is
-compatible with `ui` for every `i`.
-
-- `f(X)` and `f(h(a))` are compatible with `{X:=h(a)}`;
-- `f(X)` and `X` are incompatible;
-- `f(X)` and `g(X)` are incompatible;
-- `f(h(X))` and `f(h(a))` are compatible with {X:=a}.
diff --git a/guide/en/src/stellogen/commands.md b/guide/en/src/stellogen/commands.md
deleted file mode 100644
index f6cf11c..0000000
--- a/guide/en/src/stellogen/commands.md
+++ /dev/null
@@ -1,40 +0,0 @@
-# Commands
-
-## Comments
-
-Comments begin with `'` and are written between `'''` for multi-line comments.
-They are ignored during execution.
-
-```
-'this is a comment
-
-'''
-this is a
-multiline comment
-'''
-```
-
-## Display
-
-To display constellations, you can use the command `show` followed by a
-constellation:
-
-```
-show +a; -a b.
-```
-
-The `show` command does not execute constellation. If you want to actually
-execute the constellation and display its result, use the `show-exec` command:
-
-```
-show-exec +a; -a b.
-```
-
-## Execution trace
-
-It is possible to follow step by step the execution of a constellation:
-
-```
-ineq = +f(a); +f(b); @-f(X) -f(Y) r(X Y) | X!=Y.
-'trace ineq.
-```
diff --git a/guide/en/src/stellogen/definitions.md b/guide/en/src/stellogen/definitions.md
deleted file mode 100644
index 3389a2c..0000000
--- a/guide/en/src/stellogen/definitions.md
+++ /dev/null
@@ -1,81 +0,0 @@
-# Defining constellations
-
-## Static definitions
-
-We can name constellations that are directly written. Identifiers follow the
-same rules as for ray function symbols.
-
-```
-w = { a }.
-x = +a; -a b.
-z = -f(X).
-```
-
-When we refer to a constellation identifier, we use the prefix `#`:
-
-```
-y = #x.
-```
-
-As for application in functional programming, union of constellations is
-written with a space:
-
-```
-union1 = #x #y #z.
-```
-
-We can also add parentheses around expressions for more readability or to
-avoid syntactic ambiguity:
-
-```
-union1 = (#x #y) #z.
-```
-
-However, note that unlike in functional programming there is no defined
-ordering.
-
-> Static definitions correspond to the notion of "proof-object" in Curry-Howard
-> correspondence.
-
-## Focus
-
-We can focus all stars of a constellation by prefixing it with `@` and put
-it around parentheses:
-
-```
-x = +a; -a b.
-z = -f(X).
-union1 = @#x #z.
-```
-
-## Inequality constraints
-
-It is possible to add a sequence of inequality contraints between terms:
-
-```
-ineq = +f(a); +f(b); @-f(X) -f(Y) r(X Y) | X!=Y.
-```
-
-This makes invalid any interaction where `X` and `Y` are fully defined
-(no variable) and instanciated to the same value.
-
-Those inequalities can be separated by spaces or commas:
-
-```
-X!=Y X!=Z
-```
-
-or
-
-```
-X!=Y, X!=Z
-```
-
-## Pre-execution
-
-The execution of a constellation within a block `exec ... end` also defines
-a constellation:
-
-```
-exec +f(X); -f(a) end
-```
diff --git a/guide/en/src/stellogen/prolog.md b/guide/en/src/stellogen/prolog.md
deleted file mode 100644
index 66f0af9..0000000
--- a/guide/en/src/stellogen/prolog.md
+++ /dev/null
@@ -1,51 +0,0 @@
-# Logic programming
-
-Constellations are sort of logic programs as in Prolog. They are all-purpose
-materials.
-
-In logic programming, rays are seen as predicates, properties or relations.
-
-```
-'a is the child of b
-childOf(a b).
-```
-
-Positive rays are outputs/conclusions and negative rays are inputs/hypotheses.
-With rays, it is possible to create facts (truth of a knowledge base):
-
-```
-'knowledge base
-+childOf(a b).
-+childOf(a c).
-+childOf(c d).
-```
-
-but also inference rules:
-
-```
--childOf(X Y) -childOf(Y Z) +grandParentOf(Z X).
-```
-
-Facts and inference rules form action stars which will interact with
-*query* stars which allows to aks questions like how one queries a database:
-
-```
--childOf(X b) res(X).
-```
-
-It returns a result telling who are the children of `b`.
-
-Unlike dedicated languages like Prolog, in Stellogen you have to organize
-en trigger interactions:
-
-```
-knowledge =
-  +childOf(a b);
-  +childOf(a c);
-  +childOf(c d);
-  -childOf(X Y) -childOf(Y Z) +grandParentOf(Z X).
-
-query = -childOf(X b) res(X).
-
-show-exec #knowledge @#query.
-```
diff --git a/guide/en/src/stellogen/substitutions.md b/guide/en/src/stellogen/substitutions.md
deleted file mode 100644
index 2532958..0000000
--- a/guide/en/src/stellogen/substitutions.md
+++ /dev/null
@@ -1,36 +0,0 @@
-# Substitutions
-
-Substitutions are expressions of the form `[... => ...]` replacing an entity
-by another.
-
-## Variables
-
-Variables can be replaced by any other ray:
-
-```
-show-exec (+f(X))[X=>Y].
-show-exec (+f(X))[X=>+a(X)].
-```
-
-## Function symbols
-
-Function symbols can be replaced by other function symbols:
-
-```
-show-exec (+f(X))[+f=>+g].
-show-exec (+f(X))[+f=>f].
-```
-
-We can also omit the left or right part of `=>` to add or remove a head symbol:
-
-```
-show-exec (+f(X); f(X))[=>+a].
-show-exec (+f(X); f(X))[=>a].
-show-exec (+f(X); f(X))[+f=>].
-```
-
-## Constellation identifiers
-
-```
-show-exec (#1 #2)[#1=>+f(X) X][#2=>-f(a)].
-```
diff --git a/guide/en/src/typing/expect.md b/guide/en/src/typing/expect.md
deleted file mode 100644
index a5e6465..0000000
--- a/guide/en/src/typing/expect.md
+++ /dev/null
@@ -1,28 +0,0 @@
-# Expectations
-
-It is possible to verify whether a constellation is equal to another one
-with an expectation test:
-
-```
-x :=: +f(X).
-```
-
-In particular, passing the test of some specification such as:
-
-```
-spec t = galaxy
-  test1 = +f(X).
-  test2 = +g(X).
-end
-
-g :: t.
-```
-
-can be reformulated in an equivalent way like this:
-
-```
-t1 :=: ok.
-t1 = #g #t->test1.
-t2 :=: ok.
-t2 = #g #t->test2.
-```
diff --git a/guide/en/src/typing/spec.md b/guide/en/src/typing/spec.md
deleted file mode 100644
index 42a6151..0000000
--- a/guide/en/src/typing/spec.md
+++ /dev/null
@@ -1,154 +0,0 @@
-# Typing
-
-Typing in Stellogen illustrates key principles of transcendental syntax, where
-types are defined as *sets of tests*, themselves constructed using
-constellations. Type checking involves passing all the tests associated with a
-type.
-
-Types are represented by a galaxy, where each field corresponds to a test that
-must be passed:
-
-```
-t = galaxy
-  test1 = @-f(X) ok; -g(X).
-  test2 = @-g(X) ok; -f(X).
-end
-```
-
-It is also possible to prefix the definition with a `spec` keyword to make
-explicit that it is a specification:
-
-```
-spec t = galaxy
-  test1 = @-f(X) ok; -g(X).
-  test2 = @-g(X) ok; -f(X).
-end
-```
-
-A galaxy/constellation under test must therefore *satisfy all the tests*
-defined by the galaxy above to be of type `t`.
-
-> A type with a single test can be defined as a simple constellation.
-
-However, we still need to define what it means to:
-- be confronted with a test;
-- successfully pass a test.
-
-> In line with the Curry-Howard correspondence, types can be viewed as
-formulas or specifications. This can also be extended to Thomas Seiller's
-proposal of viewing algorithms as more sophisticated specifications.
-
-## Checkers
-
-We need to define checkers, which are "judge" galaxies that specify:
-
-- an interaction field, necessarily containing the identifiers `#tested` and `#test`. It explains how the tested and the test interact;
-- an `expect` field indicating the expected result of the interaction.
-
-For example:
-
-```
-checker = galaxy
-  interaction = #tested #test.
-  expect = ok.
-end
-```
-
-## Test-based typing
-
-We can then precede definitions with a type declaration:
-
-```
-c :: t [checker].
-c = +f(0) +g(0).
-```
-
-The constellation `c` successfully passes the `test1` and `test2` tests of `t`.
-Thus, there is no issue. We say that `c` is of type `t` or that `c` is a proof
-of the formula `t`.
-
-However, if we had a constellation that failed the tests, such as:
-
-```
-c :: t [checker].
-c = +f(0).
-```
-
-We would receive an error message indicating that a test was not passed.
-
-Here is an example of a type with a single test for a naive representation of
-natural numbers:
-
-```
-spec nat =
-  -nat(0) ok;
-  -nat(s(N)) +nat(N).
-
-0 :: nat [checker].
-0 = +nat(0).
-
-1 :: nat [checker].
-1 = +nat(s(0)).
-```
-
-We can also omit specifying the checker. In this case, the default checker is:
-
-```
-checker = galaxy
-  interaction = #tested #test.
-  expect = ok.
-end
-```
-
-This allows us to write:
-
-```
-0 :: nat.
-0 = +nat(0).
-
-1 :: nat.
-1 = +nat(s(0)).
-```
-
-## Plurality of types
-
-It is possible to associate seveeral types to a same constellation:
-- either by defining several type declarations;
-- or by writing sequences of types (separated by commas) when a same checker
-is used.
-
-For example:
-
-```
-nat2 = -nat(X) ok.
-2 :: nat [checker].
-2 :: nat2.
-2 = +nat(s(s(0))).
-```
-
-````
-3 :: nat, nat2.
-3 = +nat(s(s(s(0)))).
-```
-
-## Interface
-
-It is possible to define interfaces describing a series of identifiers with
-a corresponding type to satisfy.
-
-```
-nat_pair = interface
-  n :: nat [checker].
-  m :: nat [checker].
-end
-```
-
-It is then possible to ask for a galaxy to satisfy that interface.
-
-```
-g_pair :: nat_pair.
-g_pair = galaxy
-  n = +nat(0).
-  m = +nat(0).
-end
-```
diff --git a/guide/fr/.gitignore b/guide/fr/.gitignore
deleted file mode 100644
index 7585238..0000000
--- a/guide/fr/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-book
diff --git a/guide/fr/Makefile b/guide/fr/Makefile
deleted file mode 100644
index e255117..0000000
--- a/guide/fr/Makefile
+++ /dev/null
@@ -1,7 +0,0 @@
-all:
-	deploy
-
-deploy:
-	git pull
-	mdbook build
-	sudo rsync -aux book/. /var/www/tsguide.refl.fr/.
diff --git a/guide/fr/book.toml b/guide/fr/book.toml
deleted file mode 100644
index f401c04..0000000
--- a/guide/fr/book.toml
+++ /dev/null
@@ -1,6 +0,0 @@
-[book]
-authors = ["engboris"]
-language = "en"
-multilingual = false
-src = "src"
-title = "tsguide"
diff --git a/guide/fr/src/SUMMARY.md b/guide/fr/src/SUMMARY.md
deleted file mode 100644
index f10a660..0000000
--- a/guide/fr/src/SUMMARY.md
+++ /dev/null
@@ -1,48 +0,0 @@
-# Summary
-
-# Contexte
-
-- [Introduction](./introduction/introduction.md)
-- [Philosophie](./introduction/philosophy.md)
-- [Démarrer](./introduction/start.md)
-
-# Les constellations et leur exécution
-
-- [Unification de termes](./stellarresolution/unification.md)
-- [Etoiles et constellations](./stellarresolution/entities.md)
-- [Exécution de constellations](./stellarresolution/execution.md)
-
-# Bases de Stellogen
-
-- [Définir des constellations](./stellogen/definitions.md)
-- [Commandes](./stellogen/commands.md)
-- [Effets réactifs](./stellogen/effects.md)
-- [Substitutions](./stellogen/substitutions.md)
-- [Programmation logique](./stellogen/prolog.md)
-
-# Programmation orientée objet
-
-- [Galaxies](./objects/galaxies.md)
-- [Interfaces](./objects/interfaces.md)
-
-# Typage
-
-- [Spécifications](./typing/spec.md)
-- [Attentes](./typing/expect.md)
-
-# Programmation impérative
-
-- [Processus](./imperative/processes.md)
-
-# Machines à états
-
-- [Automate finis (TODO)](./automata/nfsa.md)
-- [Transducteurs (TODO)](./automata/transducers.md)
-- [Automates à pile (TODO)](./automata/pda.md)
-- [Machines de Turing (TODO)](./automata/turing.md)
-
-# Programmation fonctionnelle
-
-- [Lambda-calcul linéaire non typé (TODO)](./lambda/untypedlin.md)
-- [Types linéaires (TODO)](./lambda/lintypes.md)
-- [Lambda-calcul simplement typé (TODO)](./lambda/stlc.md)
diff --git a/guide/fr/src/imperative/processes.md b/guide/fr/src/imperative/processes.md
deleted file mode 100644
index 5e658d0..0000000
--- a/guide/fr/src/imperative/processes.md
+++ /dev/null
@@ -1,71 +0,0 @@
-## Processus de construction
-
-On peut enchaîner des constellations avec l'expression `process ... end` :
-
-```
-c = process
-  +n0(0).
-  -n0(X) +n1(s(X)).
-  -n1(X) +n2(s(X)).
-end
-```
-
-Cet enchaînement part de la première constellation `+n0(0)` considérée comme
-initiale. Chaque constellation suivante interagit ensuite avec le résultat
-précédent.
-
-C'est comme si nous faisions le calcul suivant :
-
-```
-c = +n0(0).
-c = @#c {-n0(X) +n1(s(X))}.
-c = @#c {-n1(X) +n2(s(X))}.
-```
-
-> C'est ce qui correspond aux tactiques dans des assistants de preuve comme Coq
-et que l'on pourrait assimiler aux programmes impératifs qui altèrent des
-représentation d'état (mémoire par exemple).
-
-> Les constructions dynamiques correspondent à la notion de "processus-preuve"
-chez Boris Eng ou de "proof-trace" chez Pablo Donato. Les processus-preuves
-construisent des objet-preuves (constellations).
-
-# Arrêt de processus
-
-Dans le résultat d'une exécution, si l'on représente les résultats par des
-rayons à polarité nulle, alors les étoiles contenant des rayons polarisés
-peuvent être interprétés comme des calculs non terminés qui pourraient être
-effacés.
-
-Pour cela, dans les processus de constructions, nous pouvons utiliser
-l'expression spéciale `#kill` :
-
-```
-c = process
-  +n0(0).
-  -n0(X) +n1(s(X)).
-  -n1(X) +n2(s(X)).
-  -n2(X) result(X); -n2(X) +n3(X).
-  #kill.
-end
-
-show-exec c.
-```
-
-Nous avons utilisé un rayon `+n3(X)` pour poursuivre des calculs
-si nous souhaitons. Le résultat est stocké dans `result(X)`.
-Mais si nous souhaitons seulement conserver le résultat et retirer toute
-autre possibilité de calcul alors on peut utiliser `#kill`.
-
-# Nettoyage de processus
-
-Il arrive parfois que l'on se retrouve avec des étoiles vides `[]` dans
-les processus. Il est possible de s'en débarrasser avec la commande `#clean` :
-
-```
-show-exec process
-  +f(0).
-  -f(X).
-  #clean.
-end
-```
diff --git a/guide/fr/src/introduction/introduction.md b/guide/fr/src/introduction/introduction.md
deleted file mode 100644
index 4199356..0000000
--- a/guide/fr/src/introduction/introduction.md
+++ /dev/null
@@ -1,37 +0,0 @@
-# Introduction
-
-Bienvenue sur le guide du langage Stellogen.
-
-**Notez que ce guide est très expérimental et est suceptible de changer
-régulièrement. Le langage présenté est tout aussi instable.**
-
-Je suis intéressé par toutes opinions, recommandations, suggestions ou simples
-questions. N'hésitez pas à me contacter à
-[boris.eng@proton.me](mailto:boris.eng@proton.me).
-
-Bonne lecture !
-
-## Comment tout a commencé
-
-Stellogen a été créé à partir des recherches de Boris Eng pour comprendre
-le programme de syntaxe transcendantale de Jean-Yves Girard.
-
-La syntaxe transcendantale propose un nouveau fondement pour la logique et
-le calcul étendant la correspondance de Curry-Howard. Dans ce nouveau
-programme, les entités logiques comme les preuves, les formules ou des
-concepts comme la vérité sont redéfinis/construits à partir d'un modèle
-de calcul élémentaire appelé "résolution stellaire", qui est une sorte
-de langage de programmation logique très flexible.
-
-Dans le but de pouvoir expérimenter avec ces idées, Eng a développé un
-interpréteur appelé "Large Star Collider (LSC)" permettant d'exécuter des
-expressions de la résolution stellaire. Il a initiallement été développé
-en Haskell puis finalement redéveloppé en OCaml.
-
-Plus tard, il a été remarqué qu'un langage de metaprogrammation était
-nécessaire pour travailler convenablement avec ces objets et notamment
-écrire des preuves de la logique linéaire (ce qui était le projet initial).
-C'est de là qu'est né le langage Stellogen.
-
-Le langage Stellogen s'est ensuite détaché petit à petit de la syntaxe
-transcendantale pour développer ses propres concepts.
diff --git a/guide/fr/src/introduction/philosophy.md b/guide/fr/src/introduction/philosophy.md
deleted file mode 100644
index 338b7f5..0000000
--- a/guide/fr/src/introduction/philosophy.md
+++ /dev/null
@@ -1,80 +0,0 @@
-# Philosophie
-
-## Connectique du sens
-
-Les types, spécifications, algorithmes et formules logiques sont des
-**questions** que l'on pose. Elles portent une *intention* qui est subjective.
-Les programmes sont des **réponses** à ces questions. Elles sont portées par
-une dynamique objective: elles peuvent être implicites et se développer
-vers une forme explicite irreductible (c'est l'exécution vers un résultat
-du calcul).
-
-La grande question est : comment savoir si l'on est face à une réponse à
-une question. Il nous faudrait une connectique de l'interaction entre
-question et réponse.
-
-## Iconoclasme et décentralisation
-
-Traditionnellement, la logique et les systèmes de types définissent des
-systèmes avec :
-- des classes d'entités (individus du premier ordre et relations);
-- des règles sémantiques (le compilateur/l'interpréteur est responsable du
-sens des expressions et l'utilisateur manipule ces expressions en suivant
-ce sens);
-- des interactions interdites;
-- des interactions autorisées.
-
-Il y a donc une préconception logique. En particulier, les compilateurs
-et interpréteurs détiennent le pouvoir sémantique : ils définissent quelles
-questions peuvent être posées et comment juger si l'on a une réponse.
-
-Stellogen tente de redonner le pouvoir sémantique à l'utilisateur, devenant
-responsable de la création du sens par des briques élémentaires qui composent
-à la fois les programmes et les types/formules/specifications.
-Les interpréteurs et compilateurs sont ensuite responsables d'un noyau basique
-assurant la bonne connexion entre ces briques mais aussi de la
-méta-programmation. Nous passons ainsi d'un rôle d'autorité sémantique à un
-rôle protocolaire et administratif de l'évaluateur.
-
-## Le sens par l'expérience
-
-Pour savoir si un programme a un certain type (si une réponse satisfait une
-question), on procède ainsi :
-- on construit un type par un ensemble de tests à passer qui sont eux-mêmes des
-programmes;
-- on construit un "juge" qui détermine ce que signifie "passer un test";
-- on connecte un programme à chaque test du type et on vérifie si le juge
-valide toutes les interactions.
-
-Cela nous donnes des garanties non-systémiques et locales similaires aux
-commandes "assert" en programmation. Nous pourrions choisir de se mettre
-dans des contextes où l'on organiserait des types et contraintes pour former
-un système.
-
-## Un ordre dans le chaos
-
-Le modèle de calcul de briques élémentaires avec lequel nous travaillons
-pourrait être qualifié de chaotique. Il est possible d'écrire des choses
-peu intuitives au résultat peu prédictible. Dans certains cas, la propriété
-de confluence n'est même pas valide (deux ordres d'exécutions mènent à deux
-résultats différents).
-
-Il y a deux manières d'obtenir un ordre dans le chaos:
-- l'émergence naturelle, locale par la création de garanties locales sur des
-bouts de programmes;
-- l'imposition d'un système fermé définissant des restrictions/contraintes
-et dans lequel seul certains types peuvent être utilisés.
-
-Stellogen souhaite laisser les deux possibilités ouvertes. Le premier choix
-permettrait une grande flexibilité et le second donnerait l'avantage de
-l'efficacité et de l'ergonomie tout en ayant des garanties plus fortes.
-
-## Vérification partielle
-
-Du point de vue de la programmation, et plus particulièrement des méthodes
-formelles, Stellogen est motivé par une vérification "partielle" s'opposant aux
-vérifications totales où l'on modéliserait entièrement un programme et ses
-propriétés pour obtenir des preuves formelles.
-
-Stellogen se concentre sur l'expressivité de contraintes locales qui pourraient
-être globalisées dans un système.
diff --git a/guide/fr/src/introduction/start.md b/guide/fr/src/introduction/start.md
deleted file mode 100644
index 8ba40eb..0000000
--- a/guide/fr/src/introduction/start.md
+++ /dev/null
@@ -1,19 +0,0 @@
-# Démarrer
-
-Pour installer l'interprêteur Stellogen, aller sur ce dépôt git :
-
-[https://github.com/engboris/stellogen](https://github.com/engboris/stellogen)
-
-Vous pouvez soit compiler à partir des [sources](https://github.com/engboris/stellogen/blob/master/README.md#build-from-sources) ou alors télécharger un
-exécutable pré-compilé :
-- Pour Linux x86-x64: [https://github.com/engboris/stellogen/releases](https://github.com/engboris/stellogen/releases)
-
-Vous pouvez ensuite simplement écrire vos programmes dans n'importe quel
-fichier texte et suivre les instructions dans le fichier [README.md](https://github.com/engboris/stellogen/blob/master/README.md#commands) du dépôt
-git pour exécuter vos programmes.
-
-Pour un aperçu rapide, n'hésitez pas à explorer :
-- [la référence syntaxique (cheat sheet)](https://github.com/engboris/stellogen/blob/master/examples/syntax.sg);
-- [les exemples de programmes](https://github.com/engboris/stellogen/tree/master/examples).
-
-Si vous êtes prêts, allons-y !
diff --git a/guide/fr/src/objects/galaxies.md b/guide/fr/src/objects/galaxies.md
deleted file mode 100644
index d4ba1bc..0000000
--- a/guide/fr/src/objects/galaxies.md
+++ /dev/null
@@ -1,25 +0,0 @@
-# Galaxies
-
-Les constellations peuvent être représentées en donnant un nom à des
-sous-constellation les composant. On appelle cela des *galaxies*.
-
-On définit les galaxies avec des blocs `galaxy ... end` contenant une
-série d'étiquettes `label =` suivit de la galaxie associée :
-
-```
-g = galaxy
-  test1 = +f(a) ok.
-  test2 = +f(b) ok.
-end
-```
-
-On accède ensuite aux champs d'une galaxie avec `->` :
-
-```
-show #g->test1.
-show #g->test2.
-```
-
-> Cela ressemble au concept de record (enregistrement) en programmation sauf
-> que lorsque les galaxies sont utilisées, elles sont représentées par leur
-> constellation sous-jacente (par oubli d'étiquettes).
diff --git a/guide/fr/src/stellarresolution/entities.md b/guide/fr/src/stellarresolution/entities.md
deleted file mode 100644
index e0469d0..0000000
--- a/guide/fr/src/stellarresolution/entities.md
+++ /dev/null
@@ -1,91 +0,0 @@
-# Etoiles et constellations
-
-## Rayons
-
-Le langage de *résolution stellaire* étend la notion de terme avec la notion
-de *rayon*. Un *rayon* est un terme où les symboles de fonction sont polarisés
-avec :
-- `+` (polarité positive);
-- `-` (polarité négative);
-- rien (polarité nulle ou absence de polarité).
-
-La *compatibilité* entre les rayons suit les mêmes règles que l'unification
-des termes sauf que :
-- au lieu de demander l'égalité `f = g` des symboles de fonction lorsque
-`f(t1, ..., tn)` est confronté à `g(u1, ..., un)`, on demande que `f` et `g`
-aient une polarité opposée (`+` contre `-`);
-- les symboles sans polarités ne peuvent pas interagir.
-
-Par exemple :
-- `+f(X)` et `-f(h(a))` sont compatibles avec `{X:=h(a)}`;
-- `f(X)` et `f(h(a))` sont incompatibles;
-- `+f(X)` et `+f(h(a))` sont incompatibles;
-- `+f(+h(X))` et `-f(-h(a))` sont compatibles avec `{X:=a}`;
-- `+f(+h(X))` et `-f(-h(+a))` sont compatibles avec `{X:=+a}`.
-
-### Chaînes de caractère
-
-Stellogen permet aussi de définir des constantes spéciales représentant des
-chaînes de caractères :
-
-```
-"this is a string literal"
-```
-
-### Séquences
-
-Il est possible d'utiliser un symbole infixe spécial `:` comme dans :
-
-```
-+w(0:1:0:1:e).
-```
-
-Il est possible de le parenthéser pour préciser la priorité (à droite par
-défaut) :
-
-```
-+w((0:(1:(0:(1:e))))).
-+w((((0:1):0):1):e).
-```
-
-## Etoiles
-
-Avec les rayons, nous pouvons former des *étoiles*. Ce sont des collections
-non ordonnées de rayons qui peuvent être entourées de crochets :
-
-```
-+f(X) -f(h(a)) +f(+h(X))
-```
-
-```
-[+f(X) -f(h(a)) +f(+h(X))]
-```
-
-L'étoile vide est notée `[]`.
-
-## Constellations
-
-Les *constellations* sont des séquences non ordonnées d'étoiles séparées
-par le symbole `;` et se terminant par un `.` :
-
-```
-+f(X) X; +f(+h(X) a f(b)).
-```
-
-Elles peuvent être entourées d'accolades :
-
-```
-{ +f(X) X; +f(+h(X) a f(b)) }.
-```
-
-Les variables sont locales à leur étoile. Cela peut être rendu explicite ainsi :
-
-```
-+f(X1) X1; +f(+h(X2) a f(b)).
-```
-
-La constellation vide est notée `{}`.
-
-Les constellations sont en fait les plus petits objets que nous pourront
-manipuler. C'est elles qui pourront être *exécutées* comme on exécute
-un programme.
diff --git a/guide/fr/src/stellarresolution/execution.md b/guide/fr/src/stellarresolution/execution.md
deleted file mode 100644
index 47444b8..0000000
--- a/guide/fr/src/stellarresolution/execution.md
+++ /dev/null
@@ -1,209 +0,0 @@
-# Exécution de constellations
-
-## Fusion d'étoiles
-
-Les étoiles interagissent entre elles par une opération appelée *fusion* (que
-l'on pourrait qualifier de protocole d'interaction), en utilisant le principe
-de la règle de *résolution de Robinson*.
-
-La fusion entre deux étoiles
-
-```
-r r1 ... rk
-```
-
-et
-
-```
-r' r1' ... rk'
-```
-
-le long de leurs rayons `r` et `r'` est définie par une nouvelle étoile :
-
-```
-theta(r1) ... theta(rk) theta(r1') ... theta(rk')
-```
-
-où `theta` est la substitution la plus générale induite par `r` et `r'`.
-
-Remarquez que:
-- `r` et `r'` sont annihilées pendant la fusion;
-- les deux étoiles fusionnent;
-- la substitution obtenue par résolution du conflit entre `r` et `r'` est
-propagée aux rayons adjacents.
-
-> **Exemple.** La fusion entre `X +f(X)` et `-f(a)` fait interagir `+f(X)`
-> et `-f(a)` ensemble pour propager la substitution `{X:=a}` sur l'unique
-> voisin `X`. Le résultat est donc `X{X:=a}` soit `a`.
-
-> Cette opération de fusion correspond à la règle de coupure pour la logique
-> du premier ordre (correspondant aussi à la règle de résolution). Cependant,
-> la différence ici est que nous sommes dans un cadre "alogique" (nos objets
-> ne portent aucun sens logique).
-
-## Exécution
-
-Cela marche à peu près comme pour la résolution d'un puzzle ou un jeu de
-fléchettes. Vous avez une constellation faites de plusieurs étoiles.
-Choisissez des *étoiles initiales*
-puis des copies des autres étoiles seront jetées dessus pour interagir par
-fusion. L'opération continue jusqu'à qu'il n'y ait plus d'interactions
-possibles (saturation).
-La constellation obtenue à la fin est le résultat de l'exécution.
-
-Plus formellement, nous séparons une constellation en deux parties pour
-l'exécuter :
-- *l'espace d'états*, un espace d'étoiles qui seront cibles de l'interaction;
-- *l'espace d'actions* qui sont des étoiles qui vont interagir avec
-les étoiles de l'espace d'états.
-
-On pourrait représenter cette séparation ainsi avec l'espace d'actions
-à gauche et l'espace d'états à droite, séparées avec le symbole `|-` :
-
-```
-a1 ... an |- s1 ... sm
-```
-
-L'exécution procède de la façon suivante :
-1. selectionner un rayon `r` d'une étoile d'état `s`;
-2. chercher toutes les connexions possibles avec des rayons `r'` d'étoiles
-d'action `a`;
-3. dupliquer `s` à droite pour chaque tel rayon `r'` trouvé car il y a
-plusieurs interactions possibles à satisfaire;
-4. remplacer chaque copie de `s` par la fusion entre `a` et `s`;
-5. répéter jusqu'à qu'il n'y a plus aucune interaction possible l'espace
-d'états.
-
-## Focus
-
-Les étoiles d'état sont préfixées par un symbole `@` :
-
-```
-@+a b; [-c d].
-```
-
-```
-+a b; [@-c d].
-```
-
-## Exemple
-
-Considérons l'exécution de la constellation suivante :
-
-```
-@+a(0(1(e)) q0);
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2).
-```
-
-Pour l'exemple, on entoure par `>>` et `<<` les rayons sélectionnés. Nous avons
-donc l'étapes suivante :
-
-```
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2);
-@+a(0(1(e)) q0).
-```
-
-Nous avons la séparation suivante :
-
-```
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2)
-|-
-+a(0(1(e)) q0)
-```
-
-Sélectionnons le premier rayon de la première étoile :
-
-```
->>-a(e q2)<< accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2)
-|-
-+a(0(1(e)) q0)
-```
-
-Il ne peut pas se connecter à `+a(0(1(e)) q0)` car le premier argument `e` est
-incompatible avec `0(1(e))`. Cependant, il peut interagir avec
-les deux étoiles suivantes (mais pas la dernière à cause d'une
-incompatibilité entre `q0` et `q1`).
-Nous effectuons une duplication et fusion suivante entre :
-
-```
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
-```
-
-et
-
-```
-+a(0(1(e)) q0)
-```
-
-donnant la substitution `{W:=1(e)}` et le résultat :
-
-```
-+a(1(e) q0);
-+a(1(e) q1)
-```
-
-Nous obtenons donc l'étape suivante :
-
-```
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2)
-|-
-+a(1(e) q0);
-+a(1(e) q1)
-```
-
-La seconde étoile d'état `+a(1(e) q1)` ne peut interagir avec aucune
-étoile d'action. Cependant on peut se focaliser sur `+a(1(e) q0)`.
-
-```
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2)
-|-
->>+a(1(e) q0)<<;
-+a(1(e) q1)
-```
-
-Il peut se connecter à `-a(1(W) q0)` avec comme substitution
-`{W:=e}` :
-
-```
--a(e q2) accept;
--a(0(W) q0) +a(W q0);
--a(0(W) q0) +a(W q1);
--a(1(W) q0) +a(W q0);
--a(0(W) q1) +a(W q2)
-|-
-+a(e q0);
-+a(1(e) q1)
-```
-
-Plus aucune interaction n'est possible.
-Le résultat de l'exécution est donc :
-
-```
-+a(e q0);
-+a(1(e) q1)
-```
diff --git a/guide/fr/src/stellarresolution/unification.md b/guide/fr/src/stellarresolution/unification.md
deleted file mode 100644
index 6d8b96d..0000000
--- a/guide/fr/src/stellarresolution/unification.md
+++ /dev/null
@@ -1,43 +0,0 @@
-# Unification de termes
-
-## Syntaxe
-
-Dans la *théorie de l'unification*, nous écrivons des *termes*. Ce sont soit :
-- des *variables* (commençant par une majuscule comme `X`, `Y` ou `Var`);
-- des *fonctions* de la forme `f(t1, ..., tn)` où `f` est un *symbole de
-fonction* (commençant par une minuscule ou un chiffre) et les expressions
-`t1`, ..., `tn` sont d'autres termes.
-
-Tous les identifiants (que cela soit pour les variables ou symboles de
-fonction) peuvent contenir les symboles `_` et `?` (mais pas au début).
-Par exemple : `is_empty?` et `X_1`.
-
-> **Exemples de termes.** `X`, `f(X)`, `h(a, X)`, `parent(X)`, `add(X, Y, Z)`.
-
-On peut aussi omettre la virgule séparant les arguments d'une fonction étant
-donné que leur absence ne produit pas d'ambiguïté. On écrirait donc
-`h(a X)` à la place de `h(a, X)`.
-
-## Principe
-
-Dans la théorie de l'unification, on dit que deux termes sont *unifiables*
-lorsqu'il existe une substitution des variables les rendant identiques.
-Par exemple, `f(X)` et `f(h(Y))` sont unifiables avec la substitution
-`{X:=h(Y)}` remplaçant `X` par `h(Y)`.
-
-Les substitutions qui nous intéressent sont celles qui sont les plus générales.
-Nous aurions pu considérer la substitution `{X:=h(c(a)); Y:=c(a)}`, tout aussi
-valide mais inutilement précise.
-
-Une autre façon de voir les choses est de voir cela comme brancher des termes
-ensemble pour vérifier s'ils sont compatibles se branchent correctement :
-- une variable `X` se branche avec tout ce qui ne contient pas `X` comme
-sous-terme, sinon nous aurions une dépendance circulaire, comme entre `X` et
-`f(X)`;
-- une fonction `f(t1, ..., tn)` est compatible avec `f(u1, ..., un)` où `ti`
-est compatible avec `ui` pour tout `i`.
-
-- `f(X)` et `f(h(a))` sont compatibles avec `{X:=h(a)}`;
-- `f(X)` et `X` sont incompatibles;
-- `f(X)` et `g(X)` sont incompatibles;
-- `f(h(X))` et `f(h(a))` sont compatibles avec `{X:=a}`.
diff --git a/guide/fr/src/stellogen/commands.md b/guide/fr/src/stellogen/commands.md
deleted file mode 100644
index bfce2b4..0000000
--- a/guide/fr/src/stellogen/commands.md
+++ /dev/null
@@ -1,41 +0,0 @@
-# Commandes
-
-## Commentaires
-
-Les commentaires commencent par `'` et sont écrits entre `'''` pour
-les commentaires multi-lignes. Ils sont ignorés pendant l'exécution.
-
-```
-'this is a comment
-
-'''
-this is a
-multiline comment
-'''
-```
-
-## Affichage
-
-Pour afficher des constellations, vous pouvez utiliser la commande `show`
-suivit d'une constellation :
-
-```
-show +a; -a b.
-```
-
-La commande `show` n'exécute pas les constellations. Si vous voulez vraiment
-exécuter la constellation et afficher son résultat, utilisez la commande
-`show-exec` :
-
-```
-show-exec +a; -a b.
-```
-
-## Trace d'exécution
-
-Il est possible de suivre pas à pas l'exécution d'une constellation :
-
-```
-ineq = +f(a); +f(b); @-f(X) -f(Y) r(X Y) | X!=Y.
-'trace ineq.
-```
diff --git a/guide/fr/src/stellogen/definitions.md b/guide/fr/src/stellogen/definitions.md
deleted file mode 100644
index 3b0f03d..0000000
--- a/guide/fr/src/stellogen/definitions.md
+++ /dev/null
@@ -1,83 +0,0 @@
-# Définir des constellations
-
-## Définitions statiques
-
-On peut nommer des constellations que l'on écrit directement. Les identifiants
-suivent les mêmes règles que pour les symboles de fonction des rayons.
-
-```
-w = a.
-x = +a; -a b.
-z = { -f(X) }.
-```
-
-Lorsque l'on se réfère à un identifiant de constellation, on utilise le
-préfixe `#`:
-
-```
-y = #x.
-```
-
-Comme pour l'application en programmation fonctionnelle, l'union de
-constellations est notée avec un espacement :
-
-```
-union1 = #x #y #z.
-```
-
-On peut aussi ajouter des parenthèses autour des expressions pour
-plus de lisibilité ou pour éviter des ambiguïtés syntaxiques :
-
-```
-union1 = (#x #y) #z.
-```
-
-Mais il faut noter que contrairement à la programmation fonctionnelle,
-il n'y a pas d'ordre défini.
-
-> Les définitions statiques correspondent à la notion "d'objet-preuve"
-> dans la correspondance de Curry-Howard.
-
-## Focus
-
-On peut mettre le focus sur toutes les étoiles d'une constellation en
-la préfixant aussi avec `@` et en l'entourant de parenthèses :
-
-```
-x = +a; -a b.
-z = -f(X).
-union1 = @#x #z.
-```
-
-## Contraintes d'inégalité
-
-Il est possible d'ajouter une séquence de contraintes d'inégalités
-entre des termes :
-
-```
-ineq = +f(a); +f(b); @-f(X) -f(Y) r(X Y) | X!=Y.
-```
-
-Cela rend invalide toute interaction où `X` et `Y` sont totalement définies
-(absence de variables) et instanciées avec la même valeur.
-
-Ces inégalités peuvent être séparées par des espaces ou des virgules :
-
-```
-X!=Y X!=Z
-```
-
-ou
-
-```
-X!=Y, X!=Z
-```
-
-## Pre-execution
-
-L'exécution d'une constellation dans un bloc `exec ... end` définit aussi
-une constellation :
-
-```
-exec +f(X); -f(a) end
-```
diff --git a/guide/fr/src/stellogen/prolog.md b/guide/fr/src/stellogen/prolog.md
deleted file mode 100644
index 1c24138..0000000
--- a/guide/fr/src/stellogen/prolog.md
+++ /dev/null
@@ -1,54 +0,0 @@
-# Programmation logique
-
-Les constellations sont des sortes de programmes logiques comme dans
-Prolog. C'est la matière élémentaire à tout faire.
-
-En programmation logique, on voit les rayons comme des prédicats, des
-propriétés ou des relations :
-
-```
-'a is the child of b
-childOf(a b).
-```
-
-Les rayons positifs sont des sorties/conclusions et les rayons négatifs
-sont des entrées/hypothèses. Avec les rayons, on peut créer des faits
-(vérités d'une base de connaissance) :
-
-```
-'knowledge base
-+childOf(a b).
-+childOf(a c).
-+childOf(c d).
-```
-
-mais aussi des règles d'inférence :
-
-```
--childOf(X Y) -childOf(Y Z) +grandParentOf(Z X).
-```
-
-Les faits et règles d'inférence vont former des étoiles d'actions qui
-vont interagir avec une étoile de *requête* qui permet de poser des
-questions comme on ferait une requête à une base de donnée :
-
-```
--childOf(X b) res(X).
-```
-
-On renvoie un résultat qui nous dira qui sont les enfants de `b`.
-
-Contrairement à des langages dédiés à ce genre d'opération comme Prolog,
-dans Stellogen, il faudra organiser et déclencher des interactions :
-
-```
-knowledge =
-  +childOf(a b);
-  +childOf(a c);
-  +childOf(c d);
-  -childOf(X Y) -childOf(Y Z) +grandParentOf(Z X).
-
-query = -childOf(X b) res(X).
-
-show-exec #knowledge @#query.
-```
diff --git a/guide/fr/src/stellogen/substitutions.md b/guide/fr/src/stellogen/substitutions.md
deleted file mode 100644
index 1232523..0000000
--- a/guide/fr/src/stellogen/substitutions.md
+++ /dev/null
@@ -1,38 +0,0 @@
-# Substitutions
-
-Les substitutions sont des expressions de la forme `[... => ...]` remplaçant
-une entité par une autre.
-
-## Variables
-
-On peut remplacer des variables par n'importe quel rayon :
-
-```
-show-exec (+f(X))[X=>Y].
-show-exec (+f(X))[X=>+a(X)].
-```
-
-## Symboles de fonction
-
-On peut remplacer les symboles de fonctions par d'autres symboles
-de fonction :
-
-```
-show-exec (+f(X))[+f=>+g].
-show-exec (+f(X))[+f=>f].
-```
-
-On peut aussi omettre la partie gauche ou droite de `=>` pour ajouter
-ou retirer un symbole de tête :
-
-```
-show-exec (+f(X); f(X))[=>+a].
-show-exec (+f(X); f(X))[=>a].
-show-exec (+f(X); f(X))[+f=>].
-```
-
-## Identificateurs de constellations
-
-```
-show-exec (#1 #2)[#1=>+f(X) X][#2=>-f(a)].
-```
diff --git a/guide/fr/src/typing/expect.md b/guide/fr/src/typing/expect.md
deleted file mode 100644
index 562da35..0000000
--- a/guide/fr/src/typing/expect.md
+++ /dev/null
@@ -1,28 +0,0 @@
-# Attentes
-
-Il est possible de vérifier si une constellation est exactement
-égale à une autre constellation avec un test d'attente :
-
-```
-x :=: +f(X).
-```
-
-En particulier, le passage des tests d'une spécification comme :
-
-```
-spec t = galaxy
-  test1 = +f(X).
-  test2 = +g(X).
-end
-
-g :: t.
-```
-
-peut être reformulé de façon équivalente ainsi :
-
-```
-t1 :=: ok.
-t1 = #g #t->test1.
-t2 :=: ok.
-t2 = #g #t->test2.
-```
diff --git a/guide/fr/src/typing/spec.md b/guide/fr/src/typing/spec.md
deleted file mode 100644
index 6978a9e..0000000
--- a/guide/fr/src/typing/spec.md
+++ /dev/null
@@ -1,158 +0,0 @@
-# Typage
-
-Le typage dans Stellogen illustre des principes majeurs de syntaxe transcendantale
-où les types sont définis comme des ensembles de *tests* eux-mêmes définis
-avec des constellations. La vérification de type implique le passage de tous
-les tests associés à un type.
-
-Les types sont donnés par une galaxie où chaque champ représentent un test à faire
-passer :
-
-```
-t = galaxy
-  test1 = @-f(X) ok; -g(X).
-  test2 = @-g(X) ok; -f(X).
-end
-```
-
-On peut aussi faire précéder la définition par `spec` pour indiquer qu'il
-s'agit d'une spécification :
-
-```
-spec t = galaxy
-  test1 = @-f(X) ok; -g(X).
-  test2 = @-g(X) ok; -f(X).
-end
-```
-
-Une galaxie/constellation *testée* doit donc être confrontée à tous les tests
-définis par la galaxie ci-dessous pour être de type `t`.
-
-> Un type avec un unique test peut être défini par une simple constellation.
-
-Il nous reste cependant à définir ce que signifient :
-- être confronté à un test;
-- passer un test avec succès.
-
-> Conformément à la correspondance de Curry-Howard, les types peuvent être vus
-comme des formules ou spécifications. On pourrait aussi étendre cela à la
-proposition de Thomas Seiller de voir les algorithmes comme des spécifications
-plus sophistiquées.
-
-## Checkers
-
-Il faut définir des *checkers* qui sont des galaxies "juges" définissant :
-- un champ `interaction` contenant un identificateur `#tested` et `#tested`.
-Ce champ explique comment faire interagir un testé et un test;
-- un champ `expect` indiquant quel est le résultat attendu par l'interaction.
-
-Par exemple :
-
-```
-checker = galaxy
-  interaction = #tested #test.
-  expect = ok.
-end
-```
-
-## Typage par test
-
-On peut ensuite faire précéder les définitions par une déclaration de type :
-
-```
-c :: t [checker].
-c = +f(0) +g(0).
-```
-
-La constellation `c` passe bel et bien les tests `test1` et `test2` de `t`.
-Il n'y a donc aucun problème. On dit donc que `c` est de type `t` ou que `c`
-est une *preuve* de la formule `t`.
-
-Cependant, si nous avions une constellation qui ne passait pas les tests, comme
-:
-
-```
-c :: t [checker].
-c = +f(0).
-```
-
-Nous aurions eu un message d'erreur nous indiquant qu'un test n'est pas passé.
-
-
-Voici un type avec un unique test pour une représentation naïve des entiers
-naturels :
-
-```
-spec nat =
-  -nat(0) ok;
-  -nat(s(N)) +nat(N).
-
-0 :: nat [checker].
-0 = +nat(0).
-
-1 :: nat [checker].
-1 = +nat(s(0)).
-```
-
-On peut aussi omettre de préciser le checker. Dans ce cas, le checker par
-défaut est :
-
-```
-checker = galaxy
-  interaction = #tested #test.
-  expect = ok.
-end
-```
-
-Cela nous permet d'écrire :
-
-```
-0 :: nat.
-0 = +nat(0).
-
-1 :: nat.
-1 = +nat(s(0)).
-```
-
-## Pluralité des types
-
-Il est possible d'associer plusieurs types à une constellation:
-- soit en définissant plusieurs déclaration de types;
-- soit en écrivant des séquences de types (séparés par des virgules) si le même
-checker est utilisé.
-
-Par exemple:
-
-```
-nat2 = -nat(X) ok.
-2 :: nat [checker].
-2 :: nat2.
-2 = +nat(s(s(0))).
-```
-
-````
-3 :: nat, nat2.
-3 = +nat(s(s(s(0)))).
-```
-
-## Interfaces
-
-Il est possible de définir des interfaces décrivant une liste d'identifiants
-devant être d'un certain type.
-
-```
-nat_pair = interface
-  n :: nat [checker].
-  m :: nat [checker].
-end
-```
-
-On peut ensuite demander à ce qu'une galaxie respecte cette interface.
-
-```
-g_pair :: nat_pair.
-g_pair = galaxy
-  n = +nat(0).
-  m = +nat(0).
-end
-```