HepLean Documentation

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.