src/rules/style/param.bend checks

raw source on the hub · import 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/rules/style/param.bend as Param

rule param: a parameter name shorter than 2 characters. A single uppercase letter is a type parameter (A, T), and a bare parameter or one typed Quant is a quantity. Locals, pattern binders and a law's for names are not parameters. A PROOF.bend's parameters are the names the law bound.

7 imports

import Base
import ../../paths.bend as Paths
import ../../src.bend as Src
import ../../finding.bend as F
import ../../syntax/bind.bend as Bind
import ../../lazy/lazy.bend as Lazy
import ../tokens.bend as T

Definitions

def check.letter source · line 14 · raw

@cs:List<&2, Char> -> Bool

one character, and a capital: a type parameter

def check.upper source · line 22 · raw

@+nm:String -> Bool

A, T, H

def check.quant source · line 28 · raw

@+note:String -> Bool

no type, or : Quant: a quantity parameter (a in List<a, A>). The note is read with its string literals cut to their quote: a : inside a string is no type

def check.short source · line 33 · raw

@+nm:String -> Bool

shorter than 2

def check.is_param source · line 37 · raw

@kk:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.BindKind -> Bool

a parameter, not a local or a pattern

def check.allowed source · line 45 · raw

@+nm:String -> @+note:String -> Bool

a type parameter or a quantity, which are allowed to be one letter

def check.go source · line 48 · raw

@binds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Bind> -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

def check.on source · line 59 · raw

@binds:List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/syntax/bind.Bind> -> @+path:String -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

def check source · line 63 · raw

@ss:0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/src.Src -> List<&2, 0x582b4b0fdf3dafdeecc8c3bfddc5e4db/src/finding.Finding>

the rule; a proof's parameters stay the law's names