1
1
mirror of https://github.com/coot/free-category.git synced 2024-09-11 14:17:30 +03:00

Added foldNatL/NilTr rewrite rule

This commit is contained in:
Marcin Szamotulski 2019-10-02 20:09:50 +01:00
parent 13bc4de0dc
commit 5ef73f172e

View File

@ -151,6 +151,9 @@ foldNatL fun (ConsTr bc ab) = fun bc . foldNatFree2 fun ab
(nat :: forall (x :: k) (y :: k). f x y -> c x y).
foldNatL nat (ConsTr f q) = nat f . foldNatL nat q
"foldNatL/NilTr" forall (nat :: forall (x :: k) (y :: k). f x y -> c x y).
foldNatL nat NilTr = id
"foldNatL/liftL"
forall (nat :: forall (x :: k) (y :: k). f x y -> c x y)
(g :: f v w)