blob: a6da0d044537f0eaa5c6ecf4a3e488b27e252db2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
|
{-# OPTIONS --safe --without-K #-}
-- List where element types depend on another list.
module Wasm.Util.List.Map where
open import Data.Fin using (Fin; zero; suc)
open import Data.List as List using (List; []; _∷_)
open import Data.Nat using (ℕ)
open import Level using (Level; _⊔_)
infixr 5 _∷_
private
variable
a b : Level
A : Set a
B : A → Set b
xs : List A
data Map {A : Set a} (B : A → Set b) : List A → Set (a ⊔ b) where
[] : Map B []
_∷_ : ∀ {x xs} (y : B x) (ys : Map B xs) → Map B (x ∷ xs)
length : Map B xs → ℕ
length {xs = xs} ys = List.length xs
lookup : (ys : Map B xs) → (i : Fin (length ys)) → B (List.lookup xs i)
lookup (y ∷ ys) zero = y
lookup (y ∷ ys) (suc i) = lookup ys i
map : ∀ {c} {C : A → Set c} → (∀ {x} → B x → C x) → Map B xs → Map C xs
map f [] = []
map f (y ∷ ys) = f y ∷ map f ys
|
