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