mirror of
https://github.com/Smaug123/agdaproofs
synced 2025-10-06 04:18:40 +00:00
20 lines
574 B
Agda
20 lines
574 B
Agda
{-# OPTIONS --safe --warning=error --without-K #-}
|
||
|
||
open import LogicalFormulae
|
||
open import Numbers.Naturals.Semiring -- for length
|
||
open import Lists.Definition
|
||
open import Lists.Fold.Fold
|
||
|
||
module Lists.Length where
|
||
|
||
length : {a : _} {A : Set a} (l : List A) → ℕ
|
||
length [] = zero
|
||
length (x :: l) = succ (length l)
|
||
|
||
length' : {a : _} {A : Set a} → (l : List A) → ℕ
|
||
length' = fold (λ _ → succ) 0
|
||
|
||
length=length' : {a : _} {A : Set a} (l : List A) → length l ≡ length' l
|
||
length=length' [] = refl
|
||
length=length' (x :: l) = applyEquality succ (length=length' l)
|