bolt
Search uses release 1.27.0.0 · 1,644 definitions
Definitions (1,644)
- def tailthe test's end, `,`, `0n` and `)`, then x kept: the finding, if any
- def at.gothe test, its head read: the finding, if any
- def ata token of kind k0, then these: a kept test?
- def hitthe finding a test makes, if any, before the rest
- def proofy.headwhat the two tokens after a def's parameters say: a `:` (no type: the def fills a law) or `->` then `{` (it returns a proof)
- def proofy.endwhat a def's header says once its parameters close
- def proofy.findoes the token close the parameters: a bracket closing at depth one?
- def proofyis the def these tokens head (after `def`) a proof?
- def item.otherwhat is skipped after a token that is no def: inside a law, from `law` on; code again from `type` or `import`; else as before
- def item.wordwhat is skipped after a keyword: a def is skipped when it is a proof
- def itemwhat is skipped after a token: a law, and a def that is a proof, never run
- def foundthe kept test a token opens, if any, outside what is skipped
- def walkevery kept test among the tokens, in order; skip says whether the tokens so far sit in a law or a def that is a proof
- def checkthe rule
- def check.rolethe rule, told the file's role (src/role.bend): a law or proof file is skipped
- def shapeare the four texts `String.from_list`, `(`, `List.reverse` and `(`?
- def ata token of text tt, then these: do the four open the shape?
- def walkevery run of the shape among the tokens, in order
- def checkthe rule
- def check.rolethe rule, told the file's role (src/role.bend): a law or proof file is skipped
- type Modewhere the length of a string literal's text is: before its opening quote, in plain text, just after a backslash, inside a `\u{..}`, or past its closing quote
- def is_cpis the char the code point?
- def len.addwhat the char adds to the length: one in plain text, but not the closing quote; nothing anywhere else
- def len.nextwhere the char leaves the length: a backslash starts an escape, a quote closes the literal, `u` after a backslash opens a `\u{..}` and `}` closes it
- def len.gothe length of the rest of a literal's text, from where it is
- def lenthe length of a string literal, its text as the lexer keeps it (quotes and escapes as written): each escape one char
- def fitsis the Nat literal's text the literal's length?
- def saywhat the finding says: the take, and the starts_with that replaces it
- type Skipwhere the scan of a take's first argument stands: inside it at a depth of brackets it opened, just past the comma that ends it, or at the bracket that closes the take before any such comma
- type Argthe argument as the finding writes it, and the tokens after its comma
- def skip.commaa comma at the depth: the argument's end at depth zero, else inside it
- def skip.closea closing bracket at the depth: the take's own at depth zero, else one bracket the argument opened
- def skip.stepwhere a token of the kind leaves the scan at the depth
- def piecea token as the finding writes it: a comma with a space after it, an operator with one on each side
- def skip.piecewhat a token adds to the argument's text, given where it leaves the scan: nothing for the comma that ends the argument
- def skipthe take's first argument, scanned from where the scan stands: what it says (acc: its pieces so far, last first) and the tokens after the comma that ends it; none when the take closes first or the tokens run out
- def dotteda dotted name: what `String.eq` is
- def tail_a.okafter the argument's comma, k, `)`, `,`, a string literal and `)`: is k the literal's length?
- def tail_athe take-first shape's end, after the argument: what the finding says
- def tail_b.okafter the argument's comma, k, `)` and `)`: is k the literal's length?
- def tail_bthe literal-first shape's end, after the argument: what the finding says
- def head_aa dotted `String.eq`, `(`, `String.take` and `(`?
- def at_a.gothe take-first shape, its head read: the end, after the argument
- def at_aa token of kind k0 and text t0, then these: the take-first shape?
- def head_ba dotted `String.eq`, `(`, a string literal, `,`, `String.take` and `(`?
- def at_b.gothe literal-first shape, its head read: the end, after the argument
- def at_ba token of kind k0 and text t0, then these: the literal-first shape?
- def eitherthe first message, else the second
- def ata token of kind k0 and text t0, then these: either shape?
- def hitthe finding a run makes, if any, before the rest
- def walkevery run of either shape among the tokens, in order
- def checkthe rule
- def check.rolethe rule, told the file's role (src/role.bend): a law or proof file is skipped
- def readsdoes a name leaf under the node read the parameter: its text, or its text then a dot?
- def endsdoes the lambda's body end after the call: the chain ends, or a comma?
- def hitare the parts a thunk of a self-call: the lead (a name parameter the call does not read), `=>`, the def's name, a `(` group, then the body's end?
- def citethe finding at the self-call's name
- def site.groupafter the parameter, `=>`, the name and its `(` group: the finding when they make a thunk of a self-call
- def site.nameafter the parameter and `=>`: the leaf that names the call
- def site.lamafter the parameter: the leaf that should be `=>`
- def sitethe finding when a node and the chain after it open a thunk of a self-call
- def lamshow many arguments of a group's kids, from here on, hold a `=>` leaf among their own nodes; seen: the argument under way does
- def onlyis a group with this open and these kids a call given exactly one lambda?
- def walkevery thunk of a self-call under the node, at any depth; lone: the node is the rest of the kids of a call given exactly one lambda
- def check.go
- def checkthe rule
- def linesthe lines of these tokens, onto acc
- def colon.kindis a token of this kind a `:`?
- def colonis the node a `:` leaf?
- def foreign.endsdoes a statement's own chain end in a `:` leaf?
- def foreign.firstis the statement an import?
- def foreign.opensdoes the body open with an import once the def's header is over?
- def foreignevery header line of the defs whose body is `import "./x.c"`, wherever the header's `->` and return type fall
- def reportabledoes a binder of this kind count?
- def usedis the binder at (line, col) the target of any use?
- def whata binder's kind, for the message
- type Cella use's target, as the index holds it
- type Hitsthe targets of the uses, as a binary trie on the low bits of each target's line, a leaf holding the cells that reach it.
- def depthhow many bits of a line the index branches on
- def patha line's way down the index: its low bits, lowest first
- def hits.cellsthe cells at a leaf, none elsewhere
- def hits.loa node's low half, empty elsewhere
- def hits.hia node's high half, empty elsewhere
- def hits.nearthe half of a node a bit goes down, empty elsewhere
- def hits.joina node whose half down a bit is sub, and the other half far
- def putthe index with one more cell, down its path
- def hits.anyis the cell at (line, col) among these?
- def findis the cell at (line, col) at the end of a path through the index?
- def index.onea use's target into the index, when it is a binder of the file
- def indexthe index of every use's target
- def seenis the binder at (line, col) the target of any use?
- def check.go
- def check.on
- def checkthe rule
- def literalis the chain exactly one number?
- def top_hasa top-level token of this text, not one nested in a group
- def array_sized`[v : T*n]` or `[v : T^d]`, and the size is a number
- def lone_numthe chain is exactly one number
- def range_count`List.replicate` / `Array.new` count at argument 2; `List.range` at the end
- def built_calla constant-size constructor, not a length taken from the data