Siegmentation Fault

@siegment

github.com/forked-from-1k…
Vrijeme pridruživanja: lipanj 2013.
33 fotografije ili videozapisa Fotografije i videozapisi

Tweetovi

Blokirali ste korisnika/cu @siegment

Jeste li sigurni da želite vidjeti te tweetove? Time nećete deblokirati korisnika/cu @siegment

  1. 30. sij

    О, видели, Coq.Float.Floats (Binary64 format of the IEEE 754-2008 standard) в кок впилили. Ждём, когда в Lean 4 тоже что‐то подобное впилят.

    1 korisnik označava da mu se sviđa
    Poništi
  2. 26. sij

    А ещё надо чинить вот такое безобразие.

    Prikaži ovu nit
    Prikaži ovu nit
    Poništi
  3. 26. sij

    С другой стороны, тут очень много места занимает описание замен в axiom schemes. (Например, «(Γ ℕ-ctx σ ℕ)» означает, что Γ будет заменена на ℕ-ctx, а σ — на ℕ.) Да и писать эти замены не очень приятно. Если их выводить автоматически, может быть, будет лучше.

    1 reply
    Prikaži ovu nit
    Prikaži ovu nit
    Poništi
  4. 26. sij

    Теория типов вручную — это, конечно, такое себе занятие. (На скриншоте вывод того, что «λ x, succ (succ x)» имеет тип «ℕ → ℕ».)

    1 reply 4 korisnika označavaju da im se sviđa
    Prikaži ovu nit
    Prikaži ovu nit
    Poništi
  5. 25. sij

    Теперь ещё и красивый синтаксис.

    1 korisnik označava da mu se sviđa
    Poništi
  6. 25. sij

    Изобретаем единицу. Сначала строим вот такую систему: Потом в контекст ℕ-ctx вводим (0 : ℕ) и (succ : ℕ→ ℕ). Далее выводим из них (succ 0 : ℕ).

    1 reply 2 korisnika označavaju da im se sviđa
    Poništi
  7. 1. sij

    Lean Together 2020, кстати, уже скоро (6—10 января).

    Poništi
  8. 1. sij

    2019 закончился, значит релиз Lean 4 ещё ближе. А ещё скоро должен наконец‐то умереть Python 2.

    Poništi
  9. 9. pro 2019.

    Не люблю обновления.

    Poništi
  10. 3. pro 2019.

    Е‐е‐е, педон!

    2 korisnika označavaju da im se sviđa
    Poništi
  11. 22. stu 2019.

    Гомоморфный образ группы изоморфен фактор‐группе по ядру гомоморфизма. (А доказательство получилось страшное.)

    3 korisnika označavaju da im se sviđa
    Poništi
  12. 3. stu 2019.

    Смотрите, какая красота (и чекается полминуты):

    1 reply 1 proslijeđeni tweet 2 korisnika označavaju da im se sviđa
    Poništi
  13. 27. lis 2019.

    Починено.

    1 korisnik označava da mu se sviđa
    Prikaži ovu nit
    Prikaži ovu nit
    Poništi
  14. 26. lis 2019.

    Теперь в Lean 4 ещё и «» вместо «». Haskell какой‐то.

    1 reply
    Prikaži ovu nit
    Prikaži ovu nit
    Poništi
  15. 23. ruj 2019.

    В Lean 4 наконец‐то завезли «» и «--run».

    1 reply 1 proslijeđeni tweet 2 korisnika označavaju da im se sviđa
    Poništi
  16. 18. kol 2019.

    Костыли для единиц измерения на Lean.

    Poništi
  17. 17. kol 2019.

    DT бывает разный.

    Poništi
  18. 7. kol 2019.

    Slowpoke news:

    Poništi
  19. 2. kol 2019.

    Оказывается, Lean Together 2020 будет.

    1 reply
    Poništi
  20. 29. srp 2019.

    Формализовал сейчас свой излюбленный приём при доказательстве на бумаге: если нужно доказать утверждение для всех натуральных чисел, то можно его доказать сначала для чётных, а потом — для нечётных. Почему‐то не удалось нагуглить подобное где‐то ещё.

    2 korisnika označavaju da im se sviđa
    Poništi

@siegment još nije objavio nijedan Tweet.

Čini se da učitavanje traje već neko vrijeme.

Twitter je možda preopterećen ili ima kratkotrajnih poteškoća u radu. Pokušajte ponovno ili potražite dodatne informacije u odjeljku Status Twittera.

    Možda bi vam se svidjelo i ovo:

    ·