Function arity reduction #
This module finds "used" parameters in a declaration, and then create an auxliary declaration that contains only used parameters. For example:
is converted into
def f._rarg (x : Nat) : Nat := let _x.1 := Nat.add x x let _x.2 := Nat.mul _x.1 _x.1 _x.2 def f (x y : Nat) : Nat := let _x.1 := f._rarg x _x.1
Note that any
f full application is going to be inlined in the next
This module has basic support for detecting "unused" variables in recursive definitions.
For example, the
y in the following definition in correctly treated as "unused"
def f (x y : Nat) : Nat := cases x | zero => x | succ _x.1 => let _x.2 := f _x.1 y let _x.3 := Nat.mul _x.2 _x.2 _x.3
This module does not have similar support for mutual recursive applications. We assume this limitation is irrelevant in practice.