Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Returning a smaller sized list
open import Agda.Builtin.Size
open import Data.Maybe.Base
data List {n} (T : Set n) (i : Size) : Set n where
[] : List T i
_∷_ : {j : Size< i} T List T j List T i
data Smaller {n} (T : Size Set n) (i : Size) : Set n where
[_] : {j : Size< i} T j Smaller T i
f : {n} {T : Set n} {i} List T i Maybe (Smaller (List T) i)
f [] = nothing
f (x ∷ xs) = just [ xs ]
g : {n} {T : Set n} {i} List T i Maybe (Smaller (List T) i)
g [] = nothing
g (_ ∷ []) = nothing
g (_ ∷ (_ ∷ xs)) = just [ xs ]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment