Loogle!

Result

Found 3 declarations mentioning Lean.Grind.AC.Expr, Nat, and Option.

• Lean.Meta.Grind.AC.Struct.mk 📋 Lean.Meta.Tactic.Grind.AC.Types
  (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (op : Lean.Expr) (neutral? : Option Lean.Expr) (assocInst : Lean.Expr) (idempotentInst? commInst? neutralInst? : Option Lean.Expr) (nextId : ℕ) (vars : Lean.PArray Lean.Expr) (varMap : Lean.PHashMap Lean.Meta.Grind.ExprPtr Lean.Grind.AC.Var) (denote : Lean.PHashMap Lean.Meta.Grind.ExprPtr Lean.Grind.AC.Expr) (denoteEntries : Lean.PArray (Lean.Expr × Lean.Grind.AC.Expr)) (queue : Lean.Meta.Grind.AC.Queue) (basis : List Lean.Meta.Grind.AC.EqCnstr) (diseqs : Lean.PArray Lean.Meta.Grind.AC.DiseqCnstr) (recheck : Bool) : Lean.Meta.Grind.AC.Struct
• Lean.Meta.Grind.AC.Struct.mk.injEq 📋 Lean.Meta.Tactic.Grind.AC.Types
  (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (op : Lean.Expr) (neutral? : Option Lean.Expr) (assocInst : Lean.Expr) (idempotentInst? commInst? neutralInst? : Option Lean.Expr) (nextId : ℕ) (vars : Lean.PArray Lean.Expr) (varMap : Lean.PHashMap Lean.Meta.Grind.ExprPtr Lean.Grind.AC.Var) (denote : Lean.PHashMap Lean.Meta.Grind.ExprPtr Lean.Grind.AC.Expr) (denoteEntries : Lean.PArray (Lean.Expr × Lean.Grind.AC.Expr)) (queue : Lean.Meta.Grind.AC.Queue) (basis : List Lean.Meta.Grind.AC.EqCnstr) (diseqs : Lean.PArray Lean.Meta.Grind.AC.DiseqCnstr) (recheck : Bool) (id✝ : ℕ) (type✝ : Lean.Expr) (u✝ : Lean.Level) (op✝ : Lean.Expr) (neutral?✝ : Option Lean.Expr) (assocInst✝ : Lean.Expr) (idempotentInst?✝ commInst?✝ neutralInst?✝ : Option Lean.Expr) (nextId✝ : ℕ) (vars✝ : Lean.PArray Lean.Expr) (varMap✝ : Lean.PHashMap Lean.Meta.Grind.ExprPtr Lean.Grind.AC.Var) (denote✝ : Lean.PHashMap Lean.Meta.Grind.ExprPtr Lean.Grind.AC.Expr) (denoteEntries✝ : Lean.PArray (Lean.Expr × Lean.Grind.AC.Expr)) (queue✝ : Lean.Meta.Grind.AC.Queue) (basis✝ : List Lean.Meta.Grind.AC.EqCnstr) (diseqs✝ : Lean.PArray Lean.Meta.Grind.AC.DiseqCnstr) (recheck✝ : Bool) : ({ id := id, type := type, u := u, op := op, neutral? := neutral?, assocInst := assocInst, idempotentInst? := idempotentInst?, commInst? := commInst?, neutralInst? := neutralInst?, nextId := nextId, vars := vars, varMap := varMap, denote := denote, denoteEntries := denoteEntries, queue := queue, basis := basis, diseqs := diseqs, recheck := recheck } = { id := id✝, type := type✝, u := u✝, op := op✝, neutral? := neutral?✝, assocInst := assocInst✝, idempotentInst? := idempotentInst?✝, commInst? := commInst?✝, neutralInst? := neutralInst?✝, nextId := nextId✝, vars := vars✝, varMap := varMap✝, denote := denote✝, denoteEntries := denoteEntries✝, queue := queue✝, basis := basis✝, diseqs := diseqs✝, recheck := recheck✝ }) = (id = id✝ ∧ type = type✝ ∧ u = u✝ ∧ op = op✝ ∧ neutral? = neutral?✝ ∧ assocInst = assocInst✝ ∧ idempotentInst? = idempotentInst?✝ ∧ commInst? = commInst?✝ ∧ neutralInst? = neutralInst?✝ ∧ nextId = nextId✝ ∧ vars = vars✝ ∧ varMap = varMap✝ ∧ denote = denote✝ ∧ denoteEntries = denoteEntries✝ ∧ queue = queue✝ ∧ basis = basis✝ ∧ diseqs = diseqs✝ ∧ recheck = recheck✝)
• Lean.Meta.Grind.AC.Struct.mk.sizeOf_spec 📋 Lean.Meta.Tactic.Grind.AC.Types
  (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (op : Lean.Expr) (neutral? : Option Lean.Expr) (assocInst : Lean.Expr) (idempotentInst? commInst? neutralInst? : Option Lean.Expr) (nextId : ℕ) (vars : Lean.PArray Lean.Expr) (varMap : Lean.PHashMap Lean.Meta.Grind.ExprPtr Lean.Grind.AC.Var) (denote : Lean.PHashMap Lean.Meta.Grind.ExprPtr Lean.Grind.AC.Expr) (denoteEntries : Lean.PArray (Lean.Expr × Lean.Grind.AC.Expr)) (queue : Lean.Meta.Grind.AC.Queue) (basis : List Lean.Meta.Grind.AC.EqCnstr) (diseqs : Lean.PArray Lean.Meta.Grind.AC.DiseqCnstr) (recheck : Bool) : sizeOf { id := id, type := type, u := u, op := op, neutral? := neutral?, assocInst := assocInst, idempotentInst? := idempotentInst?, commInst? := commInst?, neutralInst? := neutralInst?, nextId := nextId, vars := vars, varMap := varMap, denote := denote, denoteEntries := denoteEntries, queue := queue, basis := basis, diseqs := diseqs, recheck := recheck } = 1 + sizeOf id + sizeOf type + sizeOf u + sizeOf op + sizeOf neutral? + sizeOf assocInst + sizeOf idempotentInst? + sizeOf commInst? + sizeOf neutralInst? + sizeOf nextId + sizeOf vars + sizeOf varMap + sizeOf denote + sizeOf denoteEntries + sizeOf queue + sizeOf basis + sizeOf diseqs + sizeOf recheck

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO.

This is Loogle revision 187ba29 serving mathlib revision 48b7eb4