Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • Apr 22 2020 08:41
    atennapel closed #40
  • Apr 22 2020 08:41
    atennapel commented #40
  • Apr 20 2020 17:06
    5HT commented #40
  • Apr 20 2020 17:05
    5HT commented #40
  • Apr 20 2020 12:26
    atennapel opened #40
  • Apr 19 2020 10:39

    5HT on master

    PTS 3000 Merge branch 'master' of github… (compare)

  • Mar 19 2020 21:47

    5HT on master

    Update README.md (compare)

  • Mar 19 2020 16:47

    5HT on master

    Update README.md (compare)

  • Dec 29 2018 22:33

    5HT on master

    Church encoding sample (compare)

  • Dec 29 2018 15:10

    5HT on master

    fix build (compare)

  • Dec 29 2018 14:54

    5HT on master

    test infinite run travis (compare)

  • Dec 29 2018 12:53
    Travis groupoid/pts (master) errored (366)
  • Dec 29 2018 12:52
    Travis groupoid/pts (master) pending (366)
  • Dec 29 2018 12:52

    5HT on master

    Update README.md (compare)

  • Oct 24 2018 19:45
    Travis groupoid/om (master) passed (365)
  • Oct 24 2018 19:45
    Travis groupoid/om (master) pending (365)
  • Oct 24 2018 19:44

    5HT on master

    Update README.md (compare)

  • Jul 13 2018 23:41
    Travis groupoid/om (master) fixed (364)
  • Jul 13 2018 23:40
    Travis groupoid/om (master) pending (364)
  • Jul 13 2018 23:40

    5HT on master

    fix build (compare)

Zeit Raffer
@zraffer
потому что сейчас надо генерировать разные ОМ-файлы для разных универсумов
Namdak Tonpa
@5HT
ну чем проще чем лучше
там посмотри на парсеры если добавить .{ } синтаксис оно сожрет весь минимализм
а фундаментально никакой проблемы не решит
просто перенесет сложность из одного места в другое
для генерируемых парсеров нет вопросов — будет!
Zeit Raffer
@zraffer
сложность это действительно перенесет. но что касается синтаксиса, можно сделать как в Агде - передавать уровень простым аргументом, синтаксис тогда расширять не надо. просто вводится предопределенный идентификатор Level, и тайпчекер должен его понимать. и разрешить задавать что-то вроде *u как аргумент у звездочки.
Namdak Tonpa
@5HT
внутри да — никаких проблем, просто параметр в код добавить
только парсер вырастет и лексер
Zeit Raffer
@zraffer
я про парсер ОМ, чтобы не менять синтаксис
в агде нету спецсинтаксиса для уровней
Namdak Tonpa
@5HT
ты про om_parse?
Zeit Raffer
@zraffer
ну да
его можно не трогать, просто договориться, что мі расширяем тайпчекер
Namdak Tonpa
@5HT
ну так попробуй туда добавить .{ } гг
Zeit Raffer
@zraffer
блин, ты видел агду? )) там нет {}
там єто обічній аргумент
Namdak Tonpa
@5HT
типа звезда без агрументов и звезда с одним аргументом?
Zeit Raffer
@zraffer
типа да
Namdak Tonpa
@5HT
все равно там переделывать не так-то просто
даже сдвиг чего-то на единицу вправо или влево там пиздец как все портит
это же шафл )
Zeit Raffer
@zraffer
я просто вижу другую проблему - вот ЕХЕ взял файл, в котором указана Poset.{u,p} - во что он должен его оттранслировать, если u,p не заданы? а больше мне ничего не нужно ;)
Namdak Tonpa
@5HT
ну да, термы с параметрами
юниверс-термы
Zeit Raffer
@zraffer
для окончательной программы достаточно только фиксированных универсумов, которые сейчас в ОМ. но тогда мы сможем компилировать только всю программу целиком, включая main. а как компилировать библиотеку?
Namdak Tonpa
@5HT
universe variables
Zeit Raffer
@zraffer
а как єто будет на ОМ?
Namdak Tonpa
@5HT
определяться должны в модуле наверно
через один из спецсимволов
но тогда получится что на уровне рекорда будет
Zeit Raffer
@zraffer
нам нужно подставлять их в *
Computational Higher Type Theory I: Abstract Cubical Realizability
Computational Higher Type Theory II: Dependent Cubical Realizability
Zeit Raffer
@zraffer
и когда это все читать? ))
Namdak Tonpa
@5HT
это просто в историю чата
Namdak Tonpa
@5HT
а там точно нужны эти все 'posets/Data/*/Endo/=Ok' ?
а не, там индирект хитрый
Namdak Tonpa
@5HT
50 строчек на чистом CoC https://github.com/groupoid/om/blob/master/priv/posets/sec2all
Namdak Tonpa
@5HT
L. Zll,let p l
Z l i
Eric Bailey
@yurrriq
Let’s say I want to prove that addition of natural numbers is commutative.
Is such a thing possible in OM as of now?
I’m looking in priv/normal/Nat.
Namdak Tonpa
@5HT
For proving that you need Induction principle / Recursor / Equality and Inductive definition.
Something is not yet available in pure functions (OM)
Eric Bailey
@yurrriq
aha