如果瀏覽伊莉時速度太慢或無法連接,可以使用其他分流瀏覽伊莉,www01.eyny.com(02,03)。
本帖最後由 CoNsTaRwU 於 2016-12-13 01:46 AM 編輯
reverse 在數學上的意義用 Agda 表達是:- data ℕ : Set where
- zero : ℕ
- suc : ℕ → ℕ
- data Vect {l} (A : Set l) : ℕ → Set l where
- [] : Vect A zero
- _∷_ : ∀ {n} → A → Vect A n → Vect A (suc n)
- insert : ∀ {l n} {A : Set l} → A → Vect A n → Vect A (suc n)
- insert x [] = x ∷ []
- insert x (y ∷ ys) = y ∷ (insert x ys)
- reverse : ∀ {l n} {A : Set l} → Vect A n → Vect A n
- reverse (x ∷ xs) = insert x (reverse xs)
- reverse whatever = whatever
複製代碼 用 C++ 來實作的話,SGI 版本的 stl 的 std::list 對 reverse 的實作大約是像這樣(我大約寫的,不一定完全相同):- void
- M_reverse_() noexcept
- {
- list_node_base_* tmp__ = this;
- do
- {
- std::swap(tmp__->M_next_, tmp__->M_prev_);
- tmp__ = tmp__->M_prev_;
- }
- while (tmp__ != this);
- }
- void
- reverse() noexcept
- { this->M_impl_.M_node_.M_reverse_(); }
複製代碼 ... |