Index of /~nad/listings/dependent-lenses

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Agda.Builtin.Bool.html 15-Oct-2019 15:58 3.5K 
[TXT]Agda.Builtin.Cubical..>15-Oct-2019 15:58 62K 
[TXT]Agda.Builtin.Cubical..>15-Oct-2019 15:58 49K 
[TXT]Agda.Builtin.Cubical..>15-Oct-2019 15:58 4.4K 
[TXT]Agda.Builtin.Cubical..>15-Oct-2019 15:58 4.4K 
[TXT]Agda.Builtin.Equalit..>15-Oct-2019 15:58 2.4K 
[TXT]Agda.Builtin.List.html 15-Oct-2019 15:58 5.0K 
[TXT]Agda.Builtin.Nat.html 15-Oct-2019 15:58 23K 
[TXT]Agda.Builtin.Sigma.html15-Oct-2019 15:58 3.2K 
[TXT]Agda.Builtin.Unit.html 15-Oct-2019 15:58 1.6K 
[TXT]Agda.Primitive.Cubic..>15-Oct-2019 15:58 18K 
[TXT]Agda.Primitive.html 15-Oct-2019 15:58 3.8K 
[TXT]Agda.css 15-Oct-2019 15:58 1.6K 
[TXT]Bijection.html 15-Oct-2019 15:58 184K 
[TXT]Bool.html 15-Oct-2019 15:58 73K 
[TXT]Embedding.html 15-Oct-2019 15:58 66K 
[TXT]Equality.Decidable-U..>15-Oct-2019 15:58 68K 
[TXT]Equality.Decision-pr..>15-Oct-2019 15:58 84K 
[TXT]Equality.Groupoid.html 15-Oct-2019 15:58 100K 
[TXT]Equality.Instances-r..>15-Oct-2019 15:58 116K 
[TXT]Equality.Path.Isomor..>15-Oct-2019 15:58 228K 
[TXT]Equality.Path.html 15-Oct-2019 15:58 253K 
[TXT]Equality.Proposition..>15-Oct-2019 15:58 15K 
[TXT]Equality.Tactic.html 15-Oct-2019 15:58 144K 
[TXT]Equality.html 15-Oct-2019 15:58 824K 
[TXT]Equivalence.html 15-Oct-2019 15:58 653K 
[TXT]Function-universe.html 15-Oct-2019 15:58 1.6M 
[TXT]Groupoid.html 15-Oct-2019 15:58 46K 
[TXT]H-level.Closure.html 15-Oct-2019 15:58 330K 
[TXT]H-level.Truncation.C..>15-Oct-2019 15:58 584K 
[TXT]H-level.Truncation.P..>15-Oct-2019 15:58 199K 
[TXT]H-level.html 15-Oct-2019 15:58 52K 
[TXT]Injection.html 15-Oct-2019 15:58 17K 
[TXT]Lens.Dependent.html 15-Oct-2019 15:58 598K 
[TXT]Lens.Non-dependent.A..>15-Oct-2019 15:58 701K 
[TXT]Lens.Non-dependent.T..>15-Oct-2019 15:58 497K 
[TXT]Lens.Non-dependent.html15-Oct-2019 15:58 16K 
[TXT]List.html 15-Oct-2019 15:58 191K 
[TXT]Logical-equivalence...>15-Oct-2019 15:58 21K 
[TXT]Monad.html 15-Oct-2019 15:58 127K 
[TXT]Nat.html 15-Oct-2019 15:58 391K 
[TXT]Pointed-type.html 15-Oct-2019 15:58 79K 
[TXT]Preimage.html 15-Oct-2019 15:58 60K 
[TXT]Prelude.html 15-Oct-2019 15:58 124K 
[TXT]README.Record-getter..>15-Oct-2019 15:58 135K 
[TXT]README.html 15-Oct-2019 15:58 1.7K 
[TXT]Records-with-with.html 15-Oct-2019 15:58 109K 
[TXT]Surjection.html 15-Oct-2019 15:58 55K 
[TXT]Univalence-axiom.html 15-Oct-2019 15:58 640K 

README
------------------------------------------------------------------------
-- Non-dependent and dependent lenses
-- Nils Anders Danielsson
------------------------------------------------------------------------

{-# OPTIONS --cubical --safe #-}

module README where

-- Non-dependent lenses.

import Lens.Non-dependent
import Lens.Non-dependent.Traditional
import Lens.Non-dependent.Alternative

-- Dependent lenses.

import Lens.Dependent

-- Comparisons of different kinds of lenses, focusing on the
-- definition of composable record getters and setters.

import README.Record-getters-and-setters