Index of /~nad/listings/dependent-lenses

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Agda.Builtin.Bool.html 04-Jul-2019 22:53 3.5K 
[TXT]Agda.Builtin.Cubical..>04-Jul-2019 22:53 84K 
[TXT]Agda.Builtin.Cubical..>04-Jul-2019 22:53 4.4K 
[TXT]Agda.Builtin.Cubical..>04-Jul-2019 22:53 4.4K 
[TXT]Agda.Builtin.Equalit..>04-Jul-2019 22:53 2.4K 
[TXT]Agda.Builtin.List.html 04-Jul-2019 22:53 5.0K 
[TXT]Agda.Builtin.Nat.html 04-Jul-2019 22:53 23K 
[TXT]Agda.Builtin.Sigma.html04-Jul-2019 22:53 3.2K 
[TXT]Agda.Builtin.Unit.html 04-Jul-2019 22:53 1.6K 
[TXT]Agda.Primitive.Cubic..>04-Jul-2019 22:53 18K 
[TXT]Agda.Primitive.html 04-Jul-2019 22:53 3.8K 
[TXT]Agda.css 04-Jul-2019 22:53 1.5K 
[TXT]Bijection.html 04-Jul-2019 22:53 159K 
[TXT]Bool.html 04-Jul-2019 22:53 73K 
[TXT]Embedding.html 04-Jul-2019 22:53 66K 
[TXT]Equality.Decidable-U..>04-Jul-2019 22:53 68K 
[TXT]Equality.Decision-pr..>04-Jul-2019 22:53 84K 
[TXT]Equality.Groupoid.html 04-Jul-2019 22:53 100K 
[TXT]Equality.Instances-r..>04-Jul-2019 22:53 116K 
[TXT]Equality.Path.Isomor..>04-Jul-2019 22:53 229K 
[TXT]Equality.Path.html 04-Jul-2019 22:53 253K 
[TXT]Equality.Proposition..>04-Jul-2019 22:53 15K 
[TXT]Equality.Tactic.html 04-Jul-2019 22:53 144K 
[TXT]Equality.html 04-Jul-2019 22:53 804K 
[TXT]Equivalence.html 04-Jul-2019 22:53 653K 
[TXT]Function-universe.html 04-Jul-2019 22:53 1.6M 
[TXT]Groupoid.html 04-Jul-2019 22:53 46K 
[TXT]H-level.Closure.html 04-Jul-2019 22:53 312K 
[TXT]H-level.Truncation.C..>04-Jul-2019 22:53 582K 
[TXT]H-level.Truncation.P..>04-Jul-2019 22:53 199K 
[TXT]H-level.html 04-Jul-2019 22:53 51K 
[TXT]Injection.html 04-Jul-2019 22:53 17K 
[TXT]Lens.Dependent.html 04-Jul-2019 22:53 598K 
[TXT]Lens.Non-dependent.A..>04-Jul-2019 22:53 701K 
[TXT]Lens.Non-dependent.T..>04-Jul-2019 22:53 497K 
[TXT]Lens.Non-dependent.html04-Jul-2019 22:53 16K 
[TXT]List.html 04-Jul-2019 22:53 149K 
[TXT]Logical-equivalence...>04-Jul-2019 22:53 21K 
[TXT]Monad.html 04-Jul-2019 22:53 127K 
[TXT]Nat.html 04-Jul-2019 22:53 387K 
[TXT]Pointed-type.html 04-Jul-2019 22:53 79K 
[TXT]Preimage.html 04-Jul-2019 22:53 60K 
[TXT]Prelude.html 04-Jul-2019 22:53 124K 
[TXT]README.Record-getter..>04-Jul-2019 22:53 135K 
[TXT]README.html 04-Jul-2019 22:53 1.7K 
[TXT]Records-with-with.html 04-Jul-2019 22:53 107K 
[TXT]Surjection.html 04-Jul-2019 22:53 51K 
[TXT]Univalence-axiom.html 04-Jul-2019 22:53 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