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

Make 'lattice' public

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-02-18 20:18:38 -08:00
parent b1c6b4c99a
commit 6384f7006e
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/IterProd.agda
View File

@ -20,7 +20,7 @@ IterProd k = iterate k (λ t → A × t) B
-- To make iteration more convenient, package the definitions in Lattice -- To make iteration more convenient, package the definitions in Lattice
-- records, perform the recursion, and unpackage. -- records, perform the recursion, and unpackage.
private module _ where module _ where
lattice : ∀ {k : ℕ} → Lattice (IterProd k) lattice : ∀ {k : ℕ} → Lattice (IterProd k)
lattice {0} = record lattice {0} = record
{ _≈_ = _≈₂_ { _≈_ = _≈₂_