49def bobF32Power =
50 (lambda unrestricted base : F32 .
51 (lambda unrestricted exponent : Nat .
52 (nat-eliminate
53 (lambda unrestricted current : Nat . F32)
54 bobF32One
55 (lambda unrestricted predecessor : Nat .
56 (lambda unrestricted induction : F32 . (f32-multiply induction base)))
57 exponent)))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.