おい、そこのお前！ どうか私のソースを見て下さい
■ このスレッドは過去ログ倉庫に格納されています
0030デフォルトの名無しさん
NGNGfunc Fib (n) -> Nat means
:: PRE_FF:def 1
ex fib being Function of NAT, [:NAT, NAT:] st
it = (fib.n)`1 & fib.0 = [0,1] &
for n being Nat, x being Element of [: NAT, NAT :] st x = fib.n
holds fib.(n+1) = [ x`2, x`1 + x`2 ];
end;
■ このスレッドは過去ログ倉庫に格納されています