------------------------------------------------------------------------ -- The Agda standard library -- -- An alternative definition of mutually-defined lists and non-empty -- lists, using the Kleene star and plus. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Data.List.Kleene where ------------------------------------------------------------------------ -- Types and basic operations open import Data.List.Kleene.Base public