------------------------------------------------------------------------
-- The Agda standard library
--
-- Reverse view
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module Data.List.Reverse where
open import Data.List.Base as L using (List; []; _∷_; _∷ʳ_)
open import Data.List.Properties
using (unfold-reverse; reverse-involutive)
open import Function.Base using (_$_)
open import Relation.Binary.PropositionalEquality.Core
using (subst; sym)
-- If you want to traverse a list from the end, then you can use the
-- reverse view of it.
infixl 5 _∶_∶ʳ_
data Reverse {a} {A : Set a} : List A → Set a where
[] : Reverse []
_∶_∶ʳ_ : ∀ xs (rs : Reverse xs) (x : A) → Reverse (xs ∷ʳ x)
module _ {a} {A : Set a} where
reverse : (xs : List A) → Reverse (L.reverse xs)
reverse [] = []
reverse (x ∷ xs) = cast $ _ ∶ reverse xs ∶ʳ x where
cast = subst Reverse (sym $ unfold-reverse x xs)
reverseView : (xs : List A) → Reverse xs
reverseView xs = cast $ reverse (L.reverse xs) where
cast = subst Reverse (reverse-involutive xs)
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4