bolt

Releases (13)

• 1.27.0.0 indexed
• 1.26.0.0 unindexed
• 1.25.0.0 unindexed
• 1.24.0.0 unindexed
• 1.23.0.0 unindexed
• 1.22.0.0 unindexed
• 1.21.0.0 unindexed
• 1.20.0.0 unindexed
• 1.19.0.0 unindexed
• 1.18.0.0 unindexed
• 1.17.0.0 unindexed
• 1.12.0.0 unindexed
• 1.11.0.0 unindexed

Definitions (1,644)

src/rules/style/param.bend

• def check.upper`A`, `T`, `H`
• def check.quantno type, or `: Quant`: a quantity parameter (`a` in `List<a, A>`).
• def check.shortshorter than 2
• def check.is_parama parameter, not a local or a pattern
• def check.alloweda type parameter or a quantity, which are allowed to be one letter
• def check.go
• def check.on
• def checkthe rule; a proof's parameters stay the law's names
• def check.rolethe rule, told the file's role (src/role.bend): a proof file is skipped

src/rules/style/space.bend

• def has_tabis there a tab among the chars?
• def trailingdoes the line end in whitespace?
• def width_ofa token's share of its line's width; a `#|` trailer line counts nothing
• def too_widea finding when the width is over 120
• def widthsone pass over the tokens: a newline closes a line's width
• def unimportedthe tokens with every import line cut to its newline, so the width counts no import; start is whether the token opens its line, and cutting whether it is on an import line
• def check.line
• def check.go
• def checkthe rule

src/rules/style/transcong.bend

• def namedis the node a leaf of a name kind with this text?
• def parenis the node a group opened by `(`?
• def commais the node a comma leaf?
• def endsdoes the chain end here, or go on with a comma?
• def cong.callpast the `Equal.cong` leaf: a `(` group, then the argument's end
• def congdoes the chain open an argument that is exactly an `Equal.cong` call?
• def commasthe comma leaves among a chain's own nodes
• def lateis an argument with nc commas before it the fifth or the sixth?
• def fedfrom here on in a group's kids, does the fifth or sixth argument open with an `Equal.cong` call?
• def shapeare a call's kids six arguments, the fifth or the sixth an `Equal.cong`?
• def argspast the `Equal.trans` leaf: a `(` group of that shape
• def citethe finding at the `Equal.trans` leaf
• def sitethe finding when a node and the chain after it open the shape
• def bindsis the node a `=` or `<-` leaf, a let's?
• def is_letis the statement a let?
• def walkevery site under the node, at any depth; top: the node is not among a let's own nodes, nor after a `=` or `<-` leaf in its chain
• def checkthe rule

src/rules/style/wrap.bend

• type Spanwhere one parameter sits in the header: its first line, its last, its column
• type Phaseseeking the parameter list, inside it, just past its `)`, past a `->` right after it on its line, or past anything else after it
• type Actwhat a token does to the bracket depths
• type Walkthe walk: depths, where the list's `)` sat, the `(` line, and the parameter open so far (spans reversed)
• def check.brokenthe header already breaks across lines: some token of it is a newline
• def check.costone token's share of the header's width: a comment has none
• def check.addthe width so far, with one token's share added
• def check.is_colona `:` token?
• def check.width.gothe header's width through its last `:` (upto, once seen says there was one), else its whole width, a string literal counting as two and a comment none
• def check.widththe header's width, through its `:`: a comment after it does not count
• def check.starta fresh walk, before the parameter list
• def check.is_oparen`(`
• def check.is_cparen`)`
• def check.open_textan opening bracket, as the depth it raises; ANone when it is not one
• def check.on_openan opening bracket, as the depth it raises
• def check.close_texta closing bracket, as the depth it lowers; ANone when it is not one
• def check.on_closea closing bracket, as the depth it lowers
• def check.is_opan operator token
• def check.gt_charsevery char a `>`
• def check.all_gtthe text is a non-empty run of `>`
• def check.gt_counthow many `>` a run holds
• def check.ticks_ofthe angle-closes in the text, else none
• def check.opens_angle`<` or `<&` glued to a name opens type arguments
• def check.drop_closean angle close, discarded when an angle open already won
• def check.prefer_openan angle open wins over a close; otherwise the close stands
• def check.op_angle`>` runs close angles; `<` glued to a name opens one
• def check.no_anglenot an operator: no angle motion
• def check.angle_opan operator's angle motion
• def check.angle_actangle motion, when the token is an operator
• def check.keepa value used only so a branch can name it
• def check.or_angleangle motion when the token was not a bracket, else that bracket
• def check.or_closea close bracket, else angle motion
• def check.bracketsthe bracket or angle motion of a token, not the parameter list's own breaks
• def check.zerono depth is open
• def check.topthe top of the parameter list: one `(`, nothing nested
• def check.pick_open`(` at depth zero opens the parameter list; a nested one is just a paren
• def check.seek_openthe parameter list's `(`, else the token's ordinary motion
• def check.act_seekmotion while still seeking the parameter list
• def check.end_or`)` at the top of the list ends it; a nested one is just a paren
• def check.args_endthe parameter list's `)`, else the token's ordinary motion
• def check.comma_ora comma at the top of the list separates parameters
• def check.args_commaa separating comma, else the token's ordinary motion
• def check.act_argsmotion inside the parameter list
• def check.act_donepast the parameter list nothing moves
• def check.is_arrow`->`
• def check.act_shutright after the list's `)`, a `->`, or the `:` of a header with no return type (a def that fills a law), or anything else
• def check.actthe motion of one token
• def check.is_septhe parameter list's own `(`, `)` and commas are not part of a parameter
• def check.dec_uone less, and not below zero
• def check.sub`left` angle-closes applied to the depth, and not below zero
• def check.no_spana parameter that did start, onto the list
• def check.consthe open parameter, closed onto the list
• def check.rebuildthe walk rebuilt; angle-closes are applied by the caller
• def check.opened`(` opens the parameter list
• def check.ended`)` ends the parameter list, and notes where it sits
• def check.commaeda comma closes the parameter that was open
• def check.unangleda run of `>` lowers the angle depth
• def check.turna `->` on the `)` line puts the return type there; on a later line it does not
• def check.apply_onthe token's motion applied to fields already taken off the walk
• def check.applythe token's motion applied to the walk
• def check.note_extendthe same parameter, extended to this line
• def check.note_begina parameter starting here
• def check.note_onthe token continues the open parameter, or starts one
• def check.note_skipoutside the parameter list the token starts nothing
• def check.note_hereinside the parameter list, the token's position joins the open parameter