Similar to findFunDecl?
, but follows aliases (i.e., let _x.i := _x.j
).
Consider the following example
fun _f.1 ... := ...
let _x.2 := _f.1
findFunDecl? _x.2
returns none
, but findFunDecl'? _x.2
returns the declaration for _f.1
.
Lean.Compiler.LCNF.Simp.Basic
Similar to findFunDecl?
, but follows aliases (i.e., let _x.i := _x.j
).
Consider the following example
fun _f.1 ... := ...
let _x.2 := _f.1
findFunDecl? _x.2
returns none
, but findFunDecl'? _x.2
returns the declaration for _f.1
.