expr.contains_constant

Stream: lean4

[Patrick Massot]

Does anyone know the Lean 4 translation of docs#expr.contains_constant?

[Kyle Miller]

I'm not sure if there's a direct translation, but there are at least docs4#Lean.Expr.find? and docs4#Lean.Expr.isConstOf that you can wire together

[Mario Carneiro]

import Lean

def Lean.Expr.containsConst (e : Expr) (p : Name → Bool) : Bool :=
Option.isSome <| e.find? fun | .const n _ => p n | _ => false

[Patrick Massot]

Thanks to both of you!

[Scott Morrison]

Sorry, missed this earlier and re-implemented it myself, potentially more efficiently:

def containsConst (e : Expr) (p : Name → Bool) : Bool :=
e.foldConsts false (fun n b => b || p n)

The doc-string on Expr.foldConsts is /-- Apply f to every constant occurring in e once. -/, and it is using a unsafely implemented cache, presumably for performance reasons!

[Mario Carneiro]

one thing that find? will do that foldConsts won't is to exit early once the answer turns out to be true

[Mario Carneiro]

I think they are both using caching to avoid visiting the same subterm multiple times in a dag-like Expr