LINUX.ORG.RU

История изменений

Исправление quasimoto, (текущая версия) :

lambda x. new Arra<x>

open import Data.Nat
open import Data.Vec

t = λ n → replicate {n = n} 5
-- :: (n : ℕ) → Vec ℕ n

q = t 5
-- => 5 ∷ 5 ∷ 5 ∷ 5 ∷ 5 ∷ []
-- :: Vec ℕ 5

t в нормальной форме, тип установился (n : ℕ) → Vec ℕ n, проверилось, что всегда при прилёте n получится Vec размера n.

Ну как и

#include <array>

template <size_t n, typename T>
std::array<T, n> replicate(T x) {
    std::array<T, n> res;
    res.fill(x);
    return res;
}

template <size_t n> std::array<nat, n> t() {
    return replicate<n>(nat(5));
}

// for (auto x : t<5>()) printf("%ld\n", x);

тоже проверилось.

Теперь — в чём разница, примеры в студию. В распоряжении только Emacs и C-c C-l с C-c C-d от agda2-mode — даже C-c C-n не нужен, можно вычислять по C-c C-d через proxy-тип:

record Proxy {A : Set} (_ : A) : Set where

никаких IO и бакендов.

Исправление quasimoto, :

lambda x. new Arra<x>

open import Data.Nat
open import Data.Vec

t = λ n → replicate {n = n} 5
-- :: (n : ℕ) → Vec ℕ n

q = t 5
-- => 5 ∷ 5 ∷ 5 ∷ 5 ∷ 5 ∷ []
-- :: Vec ℕ 5

t в нормальной форме, тип установился (n : ℕ) → Vec ℕ n, проверилось, что всегда при прилёте n получится Vec размера n.

Ну как и

#include <array>

template <size_t n, typename T>
std::array<T, n> replicate(T x) {
    std::array<T, n> res;
    res.fill(x);
    return res;
}

template <size_t n> std::array<nat, n> t() {
    return replicate<n, nat>(5);
}

// for (auto x : t<5>()) printf("%ld\n", x);

тоже проверилось.

Теперь — в чём разница, примеры в студию. В распоряжении только Emacs и C-c C-l с C-c C-d от agda2-mode — даже C-c C-n не нужен, можно вычислять по C-c C-d через proxy-тип:

record Proxy {A : Set} (_ : A) : Set where

никаких IO и бакендов.

Исходная версия quasimoto, :

lambda x. new Arra<x>

t = λ n → replicate {n = n} 5
-- :: (n : ℕ) → Vec ℕ n

q = t 5
-- => 5 ∷ 5 ∷ 5 ∷ 5 ∷ 5 ∷ []
-- :: Vec ℕ 5

t в нормальной форме, тип установился (n : ℕ) → Vec ℕ n, проверилось, что всегда при прилёте n получится Vec размера n.

Ну как и

template <size_t n, typename T>
std::array<T, n> replicate(T x) {
    std::array<T, n> res;
    res.fill(x);
    return res;
}

template <size_t n> std::array<nat, n> t() {
    return replicate<n, nat>(5);
}

// for (auto x : t<5>()) printf("%ld\n", x);

тоже проверилось.

Теперь — в чём разница, примеры в студию. В распоряжении только Emacs и C-c C-l с C-c C-d от agda2-mode — даже C-c C-n не нужен, можно вычислять по C-c C-d через proxy-тип:

record Proxy {A : Set} (_ : A) : Set where

никаких IO и бакендов.