Implementing a lean example in Agda

MHLLeanTIZAgdaCompetition.agda

{- Lean 4
open list
#eval filter (= 4) [1, 2, 4]
-}

open import Data.Nat renaming (ℕ to Nat; _≟_ to decEqNat)
open import Data.List using (List; []; _∷_)
open import Data.Bool using (true; false)
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
  renaming (_≡_ to _==_)

filter : {A : Set} (P : A -> Set)
  {{ p : {a : A} -> Dec (P a) }} -> List A -> List A
filter P {{ p }} [] = []
filter P {{ p }} (x ∷ l) with p {x}
... | true because _ = x ∷ filter P {{p}} l
... | false because _ = filter P {{p}} l

instance
  decNat : {a b : Nat} -> Dec (a == b)
  decNat {a} {b} = decEqNat a b

example = filter (_== 4) (1 ∷ 2 ∷ 4 ∷ [])
_ = example