Search

Law-shape search

A query with a standalone _, or with brackets or ==, is a shape. It finds every law (and every def whose type is an equation) whose statement contains that shape somewhere, on either side.

• _ matches one balanced sub-term: a name, a literal, a call like List.append(a, A, xs, ys), or an operator term like 1n+m. It never spans a comma, so it never matches two arguments.
• Leading arguments can be left out. List.append(_, Nil{}) matches List.append(a, A, xs, []): a call pattern with k arguments matches the last k arguments, because quantities and types come first in Bend.
• Names match on a namespace suffix: Csv.encode_row(_) finds lib.Csv.encode_row([]), but ode_row finds nothing.
• Write constructors either way. Queries are rewritten the way bend prints terms: Nil{} is [], Zero{} is 0n, Succ{n} is 1n+n, and Con{h, t} is h <> t (a chain ending in Nil{} is a list literal).
• lhs == rhs matches a whole equation, and each side of the pattern must cover a whole side: Nat.add(_, _) == Nat.add(_, _) finds commutativity-shaped laws.
• A bare name such as List.length finds every statement that mentions it.

Examples: List.append(_, Nil{}) · Nat.add(_, 0n) · List.reverse(List.reverse(_)) · Nat.add(_, _) == Nat.add(_, _)

Names and docs

Any other query searches declaration names and doc comments. Every word must appear. Exact names rank first, then prefixes, then names containing the word, then docs.

Statements are shown as bend 2.0.36 prints them. The index covers 283 packages (latest version of each).