λ
трудоемкость точно лучше
Size: a a a
2021 March 08
AG
напоминает эксперимент симмонса с CBPV
AG
Oℕ
а как пуш валуе связан с нелиненым патерн матченгом
AG
AG
val zip_of_lin = thunk rec enzip: path -> (tree -o tree) -> F path is
fun outside: path ->
fun inside: (tree -o tree) ->
match inside with
| [hole: tree] hole ->
return outside
| [hole: tree] Node (left hole) right ->
force enzip (Left outside right) left
| [hole: tree] Node left (right hole) ->
force enzip (Right left outside) right ;;
w
Я, конечно,не источник истины, но вот вы могли бы и не врать!
AG
а как пуш валуе связан с нелиненым патерн матченгом
ну типа паттерны можно рассматривать как котермы из секвенций
AG
у кришнасвами про то был папирус
Oℕ
ну типа паттерны можно рассматривать как котермы из секвенций
это понятно, но как это помогает переиспользовакть, ссылаясь на куски патернов и матчить квошиент типы?
AG
да думаю так же как и в эгисоне этом
AG
пруфсерчем всё густо обмазать
AG
фокализация как раз с этим должна помочь
AG
странно конечно что они сами на это не ссылаются
R
val zip_of_lin = thunk rec enzip: path -> (tree -o tree) -> F path is
fun outside: path ->
fun inside: (tree -o tree) ->
match inside with
| [hole: tree] hole ->
return outside
| [hole: tree] Node (left hole) right ->
force enzip (Left outside right) left
| [hole: tree] Node left (right hole) ->
force enzip (Right left outside) right ;;
Как полюбить синтаксис чочкеля?
R
У меня травма и люблю через точечьку звать
w
У меня травма и люблю через точечьку звать
Эх, сча бы звать
ΛВ
У меня травма и люблю через точечьку звать
Пока поинтфри не пишешь то норм