Oℕ
типа Inr ( Inr ( ... ?
Size: a a a
2020 June 03
AG
ну там все через бинарные суммы да
AG
data Ty : Nat -> Type where
U : Ty n
TVar : Fin n -> Ty n
Imp : Ty Z -> Ty n -> Ty n
Prod : Ty n -> Ty n -> Ty n
Sum : Ty n -> Ty n -> Ty n
Mu : Ty (S n) -> Ty n
AG
NAT : Ty n
NAT = Mu $ Sum U (TVar FZ)
zero : Term g NAT
zero = In $ Inl TT
succ : Term {n=0} g (NAT ~> NAT)
succ = Lam $ In $ Inr $ Var Here
add : Term {n=0} g (NAT~>NAT~>NAT)
add = Lam $ Cata $ Lam $ Case (Var Here) (Var $ There $ There Here) (In $ Inr $ Var Here)
NAT = Mu $ Sum U (TVar FZ)
zero : Term g NAT
zero = In $ Inl TT
succ : Term {n=0} g (NAT ~> NAT)
succ = Lam $ In $ Inr $ Var Here
add : Term {n=0} g (NAT~>NAT~>NAT)
add = Lam $ Cata $ Lam $ Case (Var Here) (Var $ There $ There Here) (In $ Inr $ Var Here)
AG
если хочешь допустим бинарные числа, то надо как нибудь так например
BIN : Ty n
BIN = Mu $ Sum U $ Sum (TVar FZ) (TVar FZ)
BIN : Ty n
BIN = Mu $ Sum U $ Sum (TVar FZ) (TVar FZ)
AG
идея короч в том что cata это протопаттернматчинг
AG
если суммы обобщить до n-местных, и вшить в кату кейс, то получится натуральный паттернматчинг
AG
ну точнее базовый конструкт, до которого паттерн матчинг элаборируется
ZM
БЛЯЯЯЯЯЯЯ
ура, новый контент для ютупа
AD
как вы это делаете
кек
ΙΤ
если 1 то я запускаю видео спидран по тофу
куда записываться?
w
куда записываться?
Эх, сча бы записываться?
w
куда записываться?
ZM
unreal tournament
вродь начали пилить новый
ZM
я мог за 30 секунд убить двоих и умереть 3 раза
30сек, это 5-10 фрагов со снайпой и возможно сбегать за щитом или ультой
VS
да я не помню как он правильно называется, мы его лазером называли
инстагиб
VS
VS
пре альфа еще
VS
но 2 года назад играбельный был
ZM
не упустили самое важное в современной игре