DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Expose 'subset-impl' from Map

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-02-25 13:57:28 -08:00
parent 2a06e6ae2d
commit 99fc21cef2
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
Lattice/Map.agda
View File

@ -479,7 +479,7 @@ _∈k_ k m = MemProp._∈_ k (keys m)
Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v' Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m
open ImplRelation renaming (subset to subset-impl) open ImplRelation using () renaming (subset to subset-impl) public
_⊆_ : Map → Map → Set (a ⊔ℓ b) _⊆_ : Map → Map → Set (a ⊔ℓ b)
_⊆_ (kvs₁ , _) (kvs₂ , _) = subset-impl kvs₁ kvs₂ _⊆_ (kvs₁ , _) (kvs₂ , _) = subset-impl kvs₁ kvs₂