Nikaia
Menu
v0.0.1343pre-alpha GitHub

ADR-362: [v; n] Is a List Literal of n Copies of a Value That Copies, Typed by Its Use as Every List Literal Is; a List Literal of One Range Is Warned

Status: Accepted Date: October 17, 2026 Answers: how a list or an array of n equal values is written, left open by ADR-152 §4; what [0..181] deserves Related: ADR-152 D1, D2, D4 (Array[T, N], its copy rule, a literal typed by its use); ADR-135 D2 (a literal with no use is a Vec); ADR-293 (an index out of range aborts); ADR-287 (comptime); Part I 4.5, 8.3 (a value that copies, .clone()); Part III’s NK1157, NK1191, NK1201

1. Question

let safety_buffer = ???          // 181 elements, all 0
let buf: Array[u8, 4096] = ???   // a buffer with no allocation (ADR-152)

A Vec of n equal values takes a detour today - (0..<n).map(fn(_i) { 0 }).collect(), or let mut xs = [] and xs.resize(n, 0) - and an Array[T, N] takes none: its literal writes every element, so a buffer of 4096 bytes cannot be written, though ADR-152 made Array the container of the target with no allocator. [0..181], written for the numbers, is a list of one element, the range.

2. How others do it

Language n zeros Length A value that does not copy
Rust [0; 181], vec![0; n] array: a constant; Vec: any array: only Copy or a constant; vec! clones each
Zig [_]u8{0} ** 4096 a constant copied
Go [4096]byte{}, make([]int, n)   only the zero value
Swift Array(repeating: 0, count: n) any the reference copied
Python [0] * n any the same object n times ([[]] * n)

Rust’s Clippy warns on vec![0..n] (single_range_in_vec_init).

3. Options

Option Example Why it lost See
A function repeat(0, 181), filled(0) an array’s length would have to come from the result’s type; a length is inferred from arguments only (Part I 4.6) D1
An operator on a list [0] * 181 arithmetic on lists is refused (NK1191); Python’s shared-object trap D1
A new operator [0 ** 181] an operator for one use D1
Nothing new resize, map Array[T, N] stays unwritable D1
Clone a value that does not copy [name; 3] clones name three times a copy nobody wrote; Nikaia writes .clone() where a value is duplicated (Part I 8.3) D3
Refuse [0..181] an error a list of one range is rare, not wrong D5

4. Decision

D1 — [v; n] is a list literal of n copies of v.

It is a list literal, and takes its type from its use as every list literal does (ADR-152 D4): with no use it is a Vec[T], where an Array[T, N] is wanted it is that array. It is Rust’s spelling, which the lowering hands on as it is. Inside brackets the ; is unambiguous.

D2 — The length.

Where an Array[T, N] is wanted, n is a comptime integer (ADR-287) equal to N; another number, or one the build does not know, is NK1157, naming both. For a Vec, n is any whole number, worked out when the literal is reached; a negative one aborts as an index out of range does (ADR-293).

D3 — Only a value that copies.

v is worked out once. A value that copies - a number, a bool, a char, an Array or a value struct of them (Part I 8.3) - is copied n times. A value that does not copy, String, Vec or a type that owns one, is NK1280; the help writes (0..<n).map(fn(_i) { v.clone() }).collect(), where each copy is visible.

D4 — What the prover knows.

The len() of [v; n] is n, as a written literal’s is its count, and for an array N.

D5 — A list literal of one range is warned.

A list literal whose only element is a range, [0..181], is the warning NK1281: a list of one range; the help writes (0..181).collect() for the numbers and [0; 182] for that many equal values. A type written for it (let r: Vec[Range[i64]] = [0..181]) says the list is meant and silences it. A literal of several ranges is not warned.

5. Reasons

6. Consequences

Not decided here: cloning a value that does not copy, if programs ask for it; Array beyond the stack.

Decided October 17, 2026.

This site is open source. Improve this page.