Телеграмм чат группы rust_offtopic страница 11367

Size: a a a

rust_offtopic

2020 April 25

foldlRhs : (f : b -> a -> b) ->
           (init : b) ->
           (x : a) ->
           (xs : List a) ->
           foldl f init (xs ++ [x]) = f (foldl f init xs) x
foldlRhs f init x [] = Refl
foldlRhs f init x (y :: xs) = foldlRhs f (f init y) x xs

revCorrect : (xs : List a) ->
             (f : b -> a -> b) ->
             (init : b) ->
             foldl f init (revDumb xs) = foldr (flip f) init xs
revCorrect [] f init = Refl
revCorrect (x :: xs) f init = let rec = revCorrect xs f init in
                              rewrite sym rec in foldlRhs f init x (revDumb xs)

источник

23:34пожаловаться #1

Gymmasssorla in rust_offtopic

Alex Zhukovsky

foldlRhs : (f : b -> a -> b) ->
           (init : b) ->
           (x : a) ->
           (xs : List a) ->
           foldl f init (xs ++ [x]) = f (foldl f init xs) x
foldlRhs f init x [] = Refl
foldlRhs f init x (y :: xs) = foldlRhs f (f init y) x xs

revCorrect : (xs : List a) ->
             (f : b -> a -> b) ->
             (init : b) ->
             foldl f init (revDumb xs) = foldr (flip f) init xs
revCorrect [] f init = Refl
revCorrect (x :: xs) f init = let rec = revCorrect xs f init in
                              rewrite sym rec in foldlRhs f init x (revDumb xs)

а, это я видел

источник

23:34пожаловаться #2

Gymmasssorla in rust_offtopic

Alex Zhukovsky

foldlRhs : (f : b -> a -> b) ->
           (init : b) ->
           (x : a) ->
           (xs : List a) ->
           foldl f init (xs ++ [x]) = f (foldl f init xs) x
foldlRhs f init x [] = Refl
foldlRhs f init x (y :: xs) = foldlRhs f (f init y) x xs

revCorrect : (xs : List a) ->
             (f : b -> a -> b) ->
             (init : b) ->
             foldl f init (revDumb xs) = foldr (flip f) init xs
revCorrect [] f init = Refl
revCorrect (x :: xs) f init = let rec = revCorrect xs f init in
                              rewrite sym rec in foldlRhs f init x (revDumb xs)

я бы тоже не догадался через свёртки сделать, но я не понимаю почему он таким методом пошёл

источник

23:34пожаловаться #3

Gymmasssorla in rust_offtopic

типо это не очень интуитивно так верифицировать

источник

23:35пожаловаться #4

Alex Zhukovsky in rust_offtopic

по-моему норм

источник

23:35пожаловаться #5

Alex Zhukovsky in rust_offtopic

но только после олбъяснения)

источник

23:35пожаловаться #6

Alex Zhukovsky in rust_offtopic

это очень умно на самом деле

источник

23:35пожаловаться #7

Alex Zhukovsky in rust_offtopic

то что левая даёт то же что правая на развороте это очень умно

источник

23:35пожаловаться #8

Alex Zhukovsky in rust_offtopic

и вообще работает не только для списокв

источник

23:35пожаловаться #9

Bogdan in rust_offtopic

боже, как с этим бороться? если с чуваком на одинаковой позиции идшь и если начинаешь ему гворить про нейминг и опечатки — говрит что "доебываешься на ровном месте" ?)

источник

23:36пожаловаться #10

Bogdan in rust_offtopic