the update pieces' step sizes and epsilons, from the first step on
915def cgExactTable =
916 (lambda unrestricted exact : (pi unrestricted step : Nat . Nat) .
917 (nat-eliminate
918 (lambda unrestricted current : Nat . (family StdList Nat))
919 (constructor StdList StdListEmpty Nat)
920 (lambda unrestricted p : Nat .
921 (lambda unrestricted rest : (family StdList Nat) .
922 (constructor
923 StdList
924 StdListCons
925 Nat
926 (exact
927 (naturalAdd
928 coppeliusFirstStep
929 (naturalSaturatingSubtract
930 (naturalSaturatingSubtract coppeliusUpdatePieces 1)
931 p)))
932 rest)))
933 coppeliusUpdatePieces))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.