# Preview Features
Jiachen Shen and The Litex Team, 2026-05-08. Email: litexlang@outlook.com
Preview features are usable experiments. They are implemented enough to try, but their syntax and semantics may still change. For stable language concepts, read the [Manual](https://litexlang.com/doc/Manual) first.
New preview-related behavior is **appended** under [Recent additions](#recent-additions-append-only) as it lands. The struct material below describes the explicit struct-view redesign: struct definitions name tuple/cartesian-product shapes, and field access must say which struct view is being used.
## Recent additions (append-only)
Short pointers only; fuller syntax and semantics live in the in-repo [Manual](Manual.md) where noted.
### Tuple equality from projections (2026-05)
Litex can now prove `t = (a, b, ...)` from tuple shape information and component equalities such as `tuple_dim(t) = 2`, `t[1] = a`, and `t[2] = b`. This also closes goals like `forall t cart(N, N): t = (t[1], t[2])`.
### Finite set count identities (2026-05)
Litex now knows more count identities for finite set operations, including `union`, `set_minus`, and `set_diff`. See **Manual — Counting members**.
### Singleton integer intervals infer equality (2026-05)
Membership in `range(a, b)` and `closed_range(a, b)` now records the element equality directly when the integer interval has exactly one value, such as `range(1, 2)` or `closed_range(1, 1)`. `by closed_range as cases` likewise records the single equality instead of a one-branch `or`. See **Manual — Builtin Inference — Ranges** and **Manual — Closed range as cases**.
### Natural membership from nonnegative integers (2026-05)
Builtin verification can now close `x $in N` from a verified integer expression `x` together with `x >= 0` / `0 <= x`, or together with `x > 0` / `0 < x`. For example, from `a, b $in Z` and `b - a >= 0`, it can verify `b - a $in N`. See **Manual — Builtin Verification Rules — Membership Rules**.
### Structured induction proof blocks (2026-05)
`by induc` and `by strong_induc` can now split their proof into a base block and a step block. Use `prove from n = base:` for the base case, `prove induc:` for ordinary induction steps, and `prove strong_induc:` for strong induction steps. See **Manual — Induction (`by induc`, `by strong_induc`)**.
### `by transitive_prop` (2026-05)
After you prove the standard associativity-shaped `forall` for a binary user-defined `prop` or `abstract_prop`, Litex records that predicate as **transitive**. Storing a same-predicate chain (e.g. `a $p b $p c`) also stores non-adjacent consequences such as `$p(a, c)`. See **Manual — Register a transitive predicate (`by transitive_prop`)**.
### `by reflexive_prop`, `by symmetric_prop`, `by antisymmetric_prop` (2026-05)
These register basic relation properties for user-defined props only, not builtin predicates. Reflexive registrations can close `$p(a, a)`. Symmetric registrations retry positive atoms with the registered argument permutation. Antisymmetric registrations can close `a = b` from `$p(a, b)` and `$p(b, a)`. See the corresponding Manual sections and `examples/by_symmetric_reflexive_antisymmetric_prop.lit`.
### `by … as set` implementation names (2026-05)
User-facing spellings are unchanged (`by fn as set`, `by fn set as set`, `by family as set`, `by tuple as set`, …). Internal statement / `stmt_type_name` labels were aligned (e.g. `ByFnAsSetStmt`, `ByFamilyAsSetStmt`, `ByTupleAsSetStmt`, `ByFnSetAsSetStmt`).
### Explicit struct views (2026-05)
Struct usage is being redesigned around explicit views. Bare field access such as `P.x` is not part of the language. A field access must say which struct is being used, such as `&Point{P}.x` or `&Group(R){G}.op`.
The intended model is simple: `&Name(args)` is a set object, and `&Name(args){x}.field` is a named projection after proving `x $in &Name(args)`.
### Design Note: Object Meaning
When designing a new object form in Litex, the first questions are its surface shape and its well-definedness condition. Its mathematical behavior can then be supplied by builtin verification and inference rules. The AST records the shape, well-definedness checks that the expression is legal, and builtin rules explain how the object behaves in proofs.
## Struct Definitions
A `struct` definition declares a record-like shape. Each field has a name and a field type.
```litex
struct Point:
x R
y R
```
Structs may also have header parameters. The definition is stored and its field declarations are checked. In the explicit-view design, applying the struct header creates a set object such as `&Group(R)`.
```litex
abstract_prop group_property(s, zero, add, inv)
struct Group(s set):
zero s
add fn(x, y s) s
inv fn(x s) s
<=>:
$group_property(s, zero, add, inv)
```
The `<=>:` block is still part of the definition record. Its body may refer to fields by their field names, as in the example above.
## Struct Objects
`&Name(args)` is a set object. It is read as a named set-builder whose base set is the Cartesian product of the instantiated field types.
For example:
```litex
struct Point:
x R
y R
```
`&Point` is the named struct set corresponding to `cart(R, R)`.
When there is no `<=>:` block, this struct set is nonempty as soon as every field type is nonempty. For example, `&Point` is nonempty because both fields range over `R`.
For a parameterized struct:
```litex
abstract_prop group_property(s, zero, add, inv)
struct Group(s set):
zero s
add fn(x, y s) s
inv fn(x s) s
<=>:
$group_property(s, zero, add, inv)
```
`&Group(R)` is read as a named set-builder like:
```text
The field names are a naming rule for tuple projections: `zero` means `g[1]`, `add` means `g[2]`, and `inv` means `g[3]`.
## Explicit Field Access
Field access is explicit:
```text
&Point{P}.x
&Group(R){G}.add
```
The prefix says how the object is being viewed. This avoids the ambiguity of bare `P.x`, because the same tuple could be viewed through different struct definitions. A bare field name is not enough: two structs may use the same field name for different tuple positions.
```litex
struct Point1:
x R
y R
struct Point2:
y R
x R
(1, 2) $in &Point1
(1, 2) $in &Point2
&Point1{(1, 2)}.x = 1
&Point2{(1, 2)}.x = 2
```
The well-definedness check for:
```text
&Group(R){G}.add
```
reduces to proving:
```text
G $in &Group(R)
```
When `G $in &Group(R)` is known, Litex also stores the facts carried by the struct view: each explicit field access and its corresponding tuple projection belong to the field type, and each `<=>:` fact is instantiated in both forms. One form replaces field names by explicit field accesses, and the other replaces them by tuple projections. When checking tuple membership in a struct object, Litex can use the tuple components directly for the `<=>:` facts.
Once that membership is available, the field access is only a named form of tuple projection:
```text
forall G &Group(R):
&Group(R){G}.zero = G[1]
&Group(R){G}.add = G[2]
&Group(R){G}.inv = G[3]
```
If a parameter is declared with a struct object, the membership fact is available in the local context:
```text
forall G &Group(R):
&Group(R){G}.add = &Group(R){G}.add
```
Here the parameter declaration provides `G $in &Group(R)`, so the field access is well-defined inside the body.
If the explicit view becomes visually heavy, use a macro to keep the proof readable. The macro does not change the meaning; it only abbreviates the required explicit view.
```text
macro s "&StandardTwoSimplex{s}"
forall s &StandardTwoSimplex:
@s.x + @s.y + @s.z = 1
```
This is still the same as writing `&StandardTwoSimplex{s}.x`, `&StandardTwoSimplex{s}.y`, and `&StandardTwoSimplex{s}.z`.
## Current Boundaries
These syntax forms are intentionally unavailable:
- `fn(x &Point) Point`
- `P.x`
- `&Point(1, 2)`
- `by struct ...`
Use explicit struct objects and explicit field views instead:
```litex
struct Point:
x R
y R
have P &Point = (1, 2)
&Point{P}.x = P[1]
&Point{(1, 2)}.y = 2
```
This design does not add a new logical entity beyond tuples, Cartesian products, and set membership. It lets users introduce an equivalent naming rule for projections while keeping the struct view explicit.