These are chat archives for groupoid/exe

25th
Mar 2016
Zeit Raffer
@zraffer
Mar 25 2016 18:36
коммичу сюда
фича, которую я с самого начала использовал для кодировки, но она не озвучивалась - это то, что мы можем пользоваться простым черчевским вариантом для Prop и на самом деле приходится им пользоваться. из-за этого я ввожу описание макроса для этой кодировки.
конкретику можно обсуждать. ))
Namdak Tonpa
@5HT
Mar 25 2016 19:04
жесятяк:
   Type.{u+1,1,1,0,0,0} 
  record.{onEl.1, (churchAnd onEl.2 onEqu)}
:-)
Zeit Raffer
@zraffer
Mar 25 2016 19:05
как-то так
Namdak Tonpa
@5HT
Mar 25 2016 19:05
объясни эти карли брекетс в этих двух случаях
я такое первый раз вижу )
Zeit Raffer
@zraffer
Mar 25 2016 19:06
(1) имеется в виду, что тип кодируется контекстом, а не типом, и соответственно у него не один уровень универсума, а по одному уровню для каждого поля. это я вытянул из практики ручного кодирования. по другому низзя.
Namdak Tonpa
@5HT
Mar 25 2016 19:07
ага т.е. это просто последовательно ранги для полей выстроеный по прядку объявления
а во втором случае?
Zeit Raffer
@zraffer
Mar 25 2016 19:08
(2) имеется в виду, что тип кодируется двумя реальными полями, первое = первому полю поля onEl, второе = кодировке черча от второго поля поля onEl совместно с полем onEqu
т.е. есть логические поля, которые видны в ЕХЕ и физические, которые в ОМ
Namdak Tonpa
@5HT
Mar 25 2016 22:52
вот это encoding.{0}.{0}.{0} я так понимаю 3-тапл: Пропозиция, Интро и Рекурсор?
а че он тогда не вот так записан encoding.{0,0,0} для единообразности