Ой, попробовали бы эти двое Agda :) Я там пару часов транспонирование матрицы писал :)

Где-то плачет один питон. Область видимости и возможность передать неанонимную функцию

ой, можешь какой-нибудь кусочек кода показать и сказать, что он делает? жутко интересно посмотреть

Ну я только учусь... Но транспонирование матрицы вышло так _by_matrix : ℕ → ℕ → Set n by m matrix = 𝕍 (𝕍 ℕ m) n _by_matrix-of_ : ∀ {ℓ} → ℕ → ℕ → (Set ℓ) → Set ℓ n by m matrix-of A = 𝕍 (𝕍 A m) n matrix-element : ∀ {ℓ} {A : Set ℓ} {n m : ℕ} (i j : ℕ) → i < n ≡ tt → j < m ≡ tt → n by m matrix-of A → A matrix-element i j pᵢ pⱼ V = nth𝕍 j pⱼ (nth𝕍 i pᵢ V) testM : 2 by 3 matrix testM = (1 :: 2 :: 3 :: []) :: (4 :: 5 :: 6 :: []) :: [] zero-vector : (n : ℕ) → 𝕍 ℕ n zero-vector 0 = [] zero-vector (suc n) = 0 :: zero-vector n zero-matrix : (n m : ℕ) → n by m matrix zero-matrix 0 m = [] zero-matrix (suc n) m = (zero-vector m) :: (zero-matrix n m) matrix-elt : {n m : ℕ} (i j : ℕ) → i < n ≡ tt → j < m ≡ tt → n by m matrix → ℕ matrix-elt i j pᵢ pⱼ V = nth𝕍 j pⱼ (nth𝕍 i pᵢ V) d-helper : (n : ℕ) (i : ℕ) → ℕ → 𝕍 ℕ n d-helper 0 _ _ = [] d-helper (suc n) i d = (if n =ℕ i then d else 0) :: d-helper n i d diagonal-matrix-h : (d n i : ℕ) → i by n matrix diagonal-matrix-h d n 0 = [] diagonal-matrix-h d n (suc i) = d-helper n i d :: diagonal-matrix-h d n i diagonal-matrix : (d n : ℕ) → n by n matrix diagonal-matrix d n = diagonal-matrix-h d n n identity-matrix : (n : ℕ)→ n by n matrix identity-matrix n = diagonal-matrix 1 n get-column : ∀ {n m : ℕ} (j : ℕ) → j < m ≡ tt → n by m matrix → 𝕍 ℕ n get-column j p [] = [] get-column j p (row :: rows) = nth𝕍 j p row :: get-column j p rows <-suc' : ∀ {j m : ℕ} → suc j < m ≡ tt → j < m ≡ tt <-suc' {0} {suc m} p = refl <-suc' {suc j} {suc m} p = <-suc' {j} {m} p suc-h : ∀ (j m' : ℕ) → suc (j + m') ≡ j + suc m' suc-h zero m' = refl suc-h (suc j) m' rewrite suc-h j m' = refl <-add : ∀ (j m' m : ℕ) → j + m' < m ≡ tt → m' < m ≡ tt <-add zero m' m p = p <-add (suc j) m' m p = <-add j m' m (<-suc' {j + m'} {m} p) less-less-h : ∀ (j m' m : ℕ) → j + suc m' < m ≡ tt → m' < m ≡ tt less-less-h j m' m p = <-suc' {m'} {m} (<-add j (suc m') m p) transpose-h : ∀ {n m : ℕ} (m' j : ℕ) → j + m' < m ≡ tt → n by m matrix → suc j by n matrix transpose-h {n} {m} m' 0 p M = get-column {n} {m} m' p M :: [] transpose-h {n} {m} m' (suc j) p M rewrite suc-h j m' = get-column {n} {m} m' (less-less-h j m' m p) M :: transpose-h {n} {m} (suc m') j p M gg : ∀ {m : ℕ} → m + 0 < suc m ≡ tt gg {m} rewrite +0 m = <-suc m transpose : ∀ {n m : ℕ} → n by m matrix → m by n matrix transpose {n} {0} M = [] transpose {n} {suc m} M = transpose-h {n} {suc m} 0 m (gg {m}) M <-add : ∀ (j m' m : ℕ) → j + m' < m ≡ tt → m' < m ≡ tt <-add zero m' m p = p <-add (suc j) m' m p = <-add j m' m (<-suc' {j + m'} {m} p) less-less-h : ∀ (j m' m : ℕ) → j + suc m' < m ≡ tt → m' < m ≡ tt less-less-h j m' m p = <-suc' {m'} {m} (<-add j (suc m') m p) transpose-h : ∀ {n m : ℕ} (m' j : ℕ) → j + m' < m ≡ tt → n by m matrix → suc j by n matrix transpose-h {n} {m} m' 0 p M = get-column {n} {m} m' p M :: [] transpose-h {n} {m} m' (suc j) p M rewrite suc-h j m' = get-column {n} {m} m' (less-less-h j m' m p) M :: transpose-h {n} {m} (suc m') j p M gg : ∀ {m : ℕ} → m + 0 < suc m ≡ tt gg {m} rewrite +0 m = <-suc m transpose : ∀ {n m : ℕ} → n by m matrix → m by n matrix transpose {n} {0} M = [] transpose {n} {suc m} M = transpose-h {n} {suc m} 0 m (gg {m}) M

Это от чего кусочек! От Сатурна?

Ну я только учусь... Но транспонирование матрицы вышло так _by_matrix : ℕ → ℕ → Set n by m matrix = 𝕍 (𝕍 ℕ m) n _by_matrix-of_ : ∀ {ℓ} → ℕ → ℕ → (Set ℓ) → Set ℓ n by m matrix-of A = 𝕍 (𝕍 A m) n matrix-element : ∀ {ℓ} {A : Set ℓ} {n m : ℕ} (i j : ℕ) → i < n ≡ tt → j < m ≡ tt → n by m matrix-of A → A matrix-element i j pᵢ pⱼ V = nth𝕍 j pⱼ (nth𝕍 i pᵢ V) testM : 2 by 3 matrix testM = (1 :: 2 :: 3 :: []) :: (4 :: 5 :: 6 :: []) :: [] zero-vector : (n : ℕ) → 𝕍 ℕ n zero-vector 0 = [] zero-vector (suc n) = 0 :: zero-vector n zero-matrix : (n m : ℕ) → n by m matrix zero-matrix 0 m = [] zero-matrix (suc n) m = (zero-vector m) :: (zero-matrix n m) matrix-elt : {n m : ℕ} (i j : ℕ) → i < n ≡ tt → j < m ≡ tt → n by m matrix → ℕ matrix-elt i j pᵢ pⱼ V = nth𝕍 j pⱼ (nth𝕍 i pᵢ V) d-helper : (n : ℕ) (i : ℕ) → ℕ → 𝕍 ℕ n d-helper 0 _ _ = [] d-helper (suc n) i d = (if n =ℕ i then d else 0) :: d-helper n i d diagonal-matrix-h : (d n i : ℕ) → i by n matrix diagonal-matrix-h d n 0 = [] diagonal-matrix-h d n (suc i) = d-helper n i d :: diagonal-matrix-h d n i diagonal-matrix : (d n : ℕ) → n by n matrix diagonal-matrix d n = diagonal-matrix-h d n n identity-matrix : (n : ℕ)→ n by n matrix identity-matrix n = diagonal-matrix 1 n get-column : ∀ {n m : ℕ} (j : ℕ) → j < m ≡ tt → n by m matrix → 𝕍 ℕ n get-column j p [] = [] get-column j p (row :: rows) = nth𝕍 j p row :: get-column j p rows <-suc' : ∀ {j m : ℕ} → suc j < m ≡ tt → j < m ≡ tt <-suc' {0} {suc m} p = refl <-suc' {suc j} {suc m} p = <-suc' {j} {m} p suc-h : ∀ (j m' : ℕ) → suc (j + m') ≡ j + suc m' suc-h zero m' = refl suc-h (suc j) m' rewrite suc-h j m' = refl <-add : ∀ (j m' m : ℕ) → j + m' < m ≡ tt → m' < m ≡ tt <-add zero m' m p = p <-add (suc j) m' m p = <-add j m' m (<-suc' {j + m'} {m} p) less-less-h : ∀ (j m' m : ℕ) → j + suc m' < m ≡ tt → m' < m ≡ tt less-less-h j m' m p = <-suc' {m'} {m} (<-add j (suc m') m p) transpose-h : ∀ {n m : ℕ} (m' j : ℕ) → j + m' < m ≡ tt → n by m matrix → suc j by n matrix transpose-h {n} {m} m' 0 p M = get-column {n} {m} m' p M :: [] transpose-h {n} {m} m' (suc j) p M rewrite suc-h j m' = get-column {n} {m} m' (less-less-h j m' m p) M :: transpose-h {n} {m} (suc m') j p M gg : ∀ {m : ℕ} → m + 0 < suc m ≡ tt gg {m} rewrite +0 m = <-suc m transpose : ∀ {n m : ℕ} → n by m matrix → m by n matrix transpose {n} {0} M = [] transpose {n} {suc m} M = transpose-h {n} {suc m} 0 m (gg {m}) M <-add : ∀ (j m' m : ℕ) → j + m' < m ≡ tt → m' < m ≡ tt <-add zero m' m p = p <-add (suc j) m' m p = <-add j m' m (<-suc' {j + m'} {m} p) less-less-h : ∀ (j m' m : ℕ) → j + suc m' < m ≡ tt → m' < m ≡ tt less-less-h j m' m p = <-suc' {m'} {m} (<-add j (suc m') m p) transpose-h : ∀ {n m : ℕ} (m' j : ℕ) → j + m' < m ≡ tt → n by m matrix → suc j by n matrix transpose-h {n} {m} m' 0 p M = get-column {n} {m} m' p M :: [] transpose-h {n} {m} m' (suc j) p M rewrite suc-h j m' = get-column {n} {m} m' (less-less-h j m' m p) M :: transpose-h {n} {m} (suc m') j p M gg : ∀ {m : ℕ} → m + 0 < suc m ≡ tt gg {m} rewrite +0 m = <-suc m transpose : ∀ {n m : ℕ} → n by m matrix → m by n matrix transpose {n} {0} M = [] transpose {n} {suc m} M = transpose-h {n} {suc m} 0 m (gg {m}) M

На Agda просили исходник

Какой синтаксис необычный

Это страшно, но прикольно. А где это Agada используется?

Ну я только учусь... Но транспонирование матрицы вышло так _by_matrix : ℕ → ℕ → Set n by m matrix = 𝕍 (𝕍 ℕ m) n _by_matrix-of_ : ∀ {ℓ} → ℕ → ℕ → (Set ℓ) → Set ℓ n by m matrix-of A = 𝕍 (𝕍 A m) n matrix-element : ∀ {ℓ} {A : Set ℓ} {n m : ℕ} (i j : ℕ) → i < n ≡ tt → j < m ≡ tt → n by m matrix-of A → A matrix-element i j pᵢ pⱼ V = nth𝕍 j pⱼ (nth𝕍 i pᵢ V) testM : 2 by 3 matrix testM = (1 :: 2 :: 3 :: []) :: (4 :: 5 :: 6 :: []) :: [] zero-vector : (n : ℕ) → 𝕍 ℕ n zero-vector 0 = [] zero-vector (suc n) = 0 :: zero-vector n zero-matrix : (n m : ℕ) → n by m matrix zero-matrix 0 m = [] zero-matrix (suc n) m = (zero-vector m) :: (zero-matrix n m) matrix-elt : {n m : ℕ} (i j : ℕ) → i < n ≡ tt → j < m ≡ tt → n by m matrix → ℕ matrix-elt i j pᵢ pⱼ V = nth𝕍 j pⱼ (nth𝕍 i pᵢ V) d-helper : (n : ℕ) (i : ℕ) → ℕ → 𝕍 ℕ n d-helper 0 _ _ = [] d-helper (suc n) i d = (if n =ℕ i then d else 0) :: d-helper n i d diagonal-matrix-h : (d n i : ℕ) → i by n matrix diagonal-matrix-h d n 0 = [] diagonal-matrix-h d n (suc i) = d-helper n i d :: diagonal-matrix-h d n i diagonal-matrix : (d n : ℕ) → n by n matrix diagonal-matrix d n = diagonal-matrix-h d n n identity-matrix : (n : ℕ)→ n by n matrix identity-matrix n = diagonal-matrix 1 n get-column : ∀ {n m : ℕ} (j : ℕ) → j < m ≡ tt → n by m matrix → 𝕍 ℕ n get-column j p [] = [] get-column j p (row :: rows) = nth𝕍 j p row :: get-column j p rows <-suc' : ∀ {j m : ℕ} → suc j < m ≡ tt → j < m ≡ tt <-suc' {0} {suc m} p = refl <-suc' {suc j} {suc m} p = <-suc' {j} {m} p suc-h : ∀ (j m' : ℕ) → suc (j + m') ≡ j + suc m' suc-h zero m' = refl suc-h (suc j) m' rewrite suc-h j m' = refl <-add : ∀ (j m' m : ℕ) → j + m' < m ≡ tt → m' < m ≡ tt <-add zero m' m p = p <-add (suc j) m' m p = <-add j m' m (<-suc' {j + m'} {m} p) less-less-h : ∀ (j m' m : ℕ) → j + suc m' < m ≡ tt → m' < m ≡ tt less-less-h j m' m p = <-suc' {m'} {m} (<-add j (suc m') m p) transpose-h : ∀ {n m : ℕ} (m' j : ℕ) → j + m' < m ≡ tt → n by m matrix → suc j by n matrix transpose-h {n} {m} m' 0 p M = get-column {n} {m} m' p M :: [] transpose-h {n} {m} m' (suc j) p M rewrite suc-h j m' = get-column {n} {m} m' (less-less-h j m' m p) M :: transpose-h {n} {m} (suc m') j p M gg : ∀ {m : ℕ} → m + 0 < suc m ≡ tt gg {m} rewrite +0 m = <-suc m transpose : ∀ {n m : ℕ} → n by m matrix → m by n matrix transpose {n} {0} M = [] transpose {n} {suc m} M = transpose-h {n} {suc m} 0 m (gg {m}) M <-add : ∀ (j m' m : ℕ) → j + m' < m ≡ tt → m' < m ≡ tt <-add zero m' m p = p <-add (suc j) m' m p = <-add j m' m (<-suc' {j + m'} {m} p) less-less-h : ∀ (j m' m : ℕ) → j + suc m' < m ≡ tt → m' < m ≡ tt less-less-h j m' m p = <-suc' {m'} {m} (<-add j (suc m') m p) transpose-h : ∀ {n m : ℕ} (m' j : ℕ) → j + m' < m ≡ tt → n by m matrix → suc j by n matrix transpose-h {n} {m} m' 0 p M = get-column {n} {m} m' p M :: [] transpose-h {n} {m} m' (suc j) p M rewrite suc-h j m' = get-column {n} {m} m' (less-less-h j m' m p) M :: transpose-h {n} {m} (suc m') j p M gg : ∀ {m : ℕ} → m + 0 < suc m ≡ tt gg {m} rewrite +0 m = <-suc m transpose : ∀ {n m : ℕ} → n by m matrix → m by n matrix transpose {n} {0} M = [] transpose {n} {suc m} M = transpose-h {n} {suc m} 0 m (gg {m}) M

public class task2 { public static void main(String[] args) { int[] prime = new int [100];} boolean isPrime(int n){ if (n > 1)//if (n > 1) { for (int i = 2; i < n; i++)// в цикле перебираем числа от 2 до n - 1 if (n % i == 0) // если n делится без остатка на i - возвращаем false (число не простое) false; // если программа дошла до данного оператора, то возвращаем true (число простое) - проверка пройдена return true; } else if ()// иначе возвращаем false (число не простое) return false; } if (isPrime = true){ int[] prime = isPrime; System.out.println(prime); } }

ну кстати не так уж сложно прочитать, если знать синтаксис, а так мозг ломается

разве паттерн-матчинг это что-то сложное?

https://github.com/cedille/ial/blob/master/braun-tree.agda А это красно-чёрное дерево на Agda

разве паттерн-матчинг это что-то сложное?

Т.е. все правила /возможные варианты использования как то тяжко пока осознать.

import java.util.Arrays; import static java.lang.Math.sqrt; public class Main { public static void main(String[] args) { int[] primeNumbers = new int[100]; primeNumbers[0] = 1; for (int i = 1; i < primeNumbers.length; i++) {//заполняем массив for (int n = primeNumbers[i - 1] + 1; ; n++) { //ищем следующее простое число отталкиваясь от последнего заполненного boolean isPrime = isPrime(n); if (isPrime) { primeNumbers[i] = n; break; } } } System.out.println(Arrays.toString(primeNumbers)); } static boolean isPrime(int n) { //проверяем число на простоту for (int i = 2; i <= sqrt(n); i++) { if (n % i == 0) { return false; } } return true; } }

спасибо огромное

ибо это основы, без этого дальше не уедешь

У меня есть переменные булевые такие: isMobile(смартфоны), isTablet(планшеты), isDesktop(мониторы ПК), а как бы вы назвали переменную, которая обозначает смартфоны и планшеты вместе?

У меня есть переменные булевые такие: isMobile(смартфоны), isTablet(планшеты), isDesktop(мониторы ПК), а как бы вы назвали переменную, которая обозначает смартфоны и планшеты вместе?

У меня есть переменные булевые такие: isMobile(смартфоны), isTablet(планшеты), isDesktop(мониторы ПК), а как бы вы назвали переменную, которая обозначает смартфоны и планшеты вместе?

А как стать программистом?

И станешь

А как стать программистом?

Уже учу html, через десяток уроков начинается по списку в этом же курсе css. Можно ли после этого начинать что то другое? Или надо годик изучать только это?

Как только в трудовом договоре будет написано, что ты программист, так и станешь программистом, все просто.

О, здравствуйте, только сегодня хотел вас найти

Учи JS

Вот всегда хотелось спросить "на чем основываются подобного рода советы"?