EnvSearch — "loogle-lite" local declaration search over the elaborated env

This module provides two #…Find commands that query the elaborated environment (every declaration reachable from the current imports), not the source text. This is precisely the discovery problem grep cannot solve: grep searches resolved syntax; these commands search resolved names and pretty-printed types. So questions like

• "which defs produce a Com jasminDialect?" (the result type matters, not the spelling in any one file), or
• "which theorems mention thirToJasmin?"

are answered directly, even when the producing declaration lives in a different file, is generated, or names its type via an abbreviation that grep would miss.

Commands

• #nameFind "substr" (cap)? — list every declaration whose name contains substr (case-insensitive), printed as name : <type>. The name filter is cheap, so this scans the whole environment. Internal/auto-generated names (_-mangled, .proof_…, ._…, .match_…, .eq_…, .brecOn, …) are skipped. Result count is capped (default 40); pass a trailing Nat to change the cap.

• #typeFind "typeSubstr" (in <Namespace>)? (cap)? — list every declaration whose pretty-printed type contains typeSubstr, printed as name : <type>. Pretty-printing every type in a Mathlib-scale environment is expensive, so a namespace prefilter is strongly recommended: with in <Namespace> only declarations whose name starts with that namespace are pretty-printed and matched (default namespace prefix: CatCrypt). Cap default is 40; pass a trailing Nat to change it.

• #docFind "substr" (in <Namespace>)? (cap)? — list every declaration whose docstring contains substr (case-insensitive), printed as name : <docstring snippet around the match>. This is the concept search: the human-readable capability descriptions in this project live in docstrings (e.g. "verified Pippenger bucket-accumulation MSM equals the naive sum"), which #nameFind (names only) and #typeFind (types only) both miss — so a cryptically-named theorem like bucketMsm_eq_msm is found by asking for "Pippenger" or "bucket". Docstring lookup is cheap (an env-extension hit, no pretty-printing), so the whole environment under the namespace prefilter (default CatCrypt) is scanned. Cap default 40. Use this BEFORE writing a new def/theorem — it is the fastest way to catch that the capability already exists under an unguessable name.

How an agent uses this

Create (or reuse) a scratch file that imports CatCrypt.Tactic.EnvSearch together with whatever module brings the declarations of interest into scope, edit the #…Find query line, and read the resulting info diagnostic via mcp__lean-lsp__lean_diagnostic_messages. Each command emits its hits as a single multi-line logInfo, so one diagnostic carries the whole answer.

Example queries

import CatCrypt.Tactic.EnvSearch
import CatCrypt.Crypto.SecureCompilation.ThirToComFront

-- defs/theorems whose *type* mentions `Com jasminDialect`, under `CatCrypt`:
#typeFind "Com jasminDialect" in CatCrypt

-- everything named like the front lowering:
#nameFind "thirToJasmin"

-- raise the cap and search a narrower namespace:
#typeFind "SPComp" in CatCrypt.Crypto.UOV 80

def CatCrypt.Tactic.EnvSearch.isInternalName (n : Lean.Name) : Bool

Heuristic: is n an internal / auto-generated name we want to hide? Covers the compiler-mangled and proof-helper families that swamp a raw name-substring scan without being useful search hits.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Tactic.EnvSearch.containsCI (hay needle : String) : Bool

Lowercase substring containment test.

Equations

• CatCrypt.Tactic.EnvSearch.containsCI hay needle = decide ((hay.toLower.splitOn needle.toLower).length > 1)

def CatCrypt.Tactic.EnvSearch.isIdentChar (c : Char) : Bool

Characters that can legitimately appear inside a (possibly dotted) Lean identifier. Anything else is a separator when we collapse qualified names to their final component.

Equations

• CatCrypt.Tactic.EnvSearch.isIdentChar c = (c.isAlphanum || c == '_' || c == '.' || c == '\'' || c == '!' || c == '?')

def CatCrypt.Tactic.EnvSearch.collapseQualified (s : String) : String

Collapse every dotted qualified identifier in s to its final component (A.B.foo ↦ foo), leaving all other text intact. This lets #typeFind "Com jasminDialect" match a type the pretty-printer rendered fully-qualified as …VIR.Com …VIR.jasminDialect, without the caller having to open the right namespaces or spell the full path.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Tactic.EnvSearch.ppTypeString (ty : Lean.Expr) : Lean.MetaM String

Pretty-print a declaration's type to a single-line String, with binders and a generous width so the substring match sees a stable rendering.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Tactic.EnvSearch.fmtHit (n : Lean.Name) (tyStr : String) : String

Format one hit as name : type.

Equations

• CatCrypt.Tactic.EnvSearch.fmtHit n tyStr = toString " " ++ toString n ++ toString " : " ++ toString tyStr

def CatCrypt.Tactic.EnvSearch.docSnippet (doc needle : String) : String

Flatten a docstring to one line (trim each line, drop blanks, single-space join), then return a ~180-char window around the first case-insensitive occurrence of needle (starting a little before it for context). Used to render a #docFind hit on one line.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Tactic.EnvSearch.renderResult (cmd query : String) (hits : Array String) (scanned cap : Nat) (truncated : Bool) : Lean.MessageData

Render the accumulated hit lines (or the empty-result message) for command cmd with the given query, noting truncation if the cap was reached.

Equations

• One or more equations did not get rendered due to their size.

#nameFind

def CatCrypt.Tactic.EnvSearch.«command#nameFind__» : Lean.ParserDescr

#nameFind "substr" (cap)? — declarations whose name contains substr (case-insensitive). Scans the whole environment (cheap, name-only); skips internal/auto-generated names; prints name : <type>. Cap default 40.

Equations

• One or more equations did not get rendered due to their size.

#typeFind

def CatCrypt.Tactic.EnvSearch.«command#typeFind_In__» : Lean.ParserDescr

#typeFind "typeSubstr" (in <Namespace>)? (cap)? — declarations whose pretty-printed type contains typeSubstr. A namespace prefilter keeps the (expensive) pretty-printing bounded; default prefix CatCrypt. Prints name : <type>. Cap default 40.

Equations

• One or more equations did not get rendered due to their size.

#docFind — search the human-readable capability descriptions

def CatCrypt.Tactic.EnvSearch.«command#docFind_In__» : Lean.ParserDescr

#docFind "substr" (in <Namespace>)? (cap)? — declarations whose docstring contains substr (case-insensitive). The CONCEPT search: capability descriptions live in docstrings, which #nameFind/#typeFind miss. Namespace prefilter (default CatCrypt); prints name : <snippet>. Cap default 40. Run this BEFORE building a new declaration.

Equations

• One or more equations did not get rendered due to their size.