Index of /~nad/listings/dependent-lenses

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Agda.css 20-Mar-2018 18:39 1.2K 
[TXT]Agda.Builtin.Unit.html 20-Mar-2018 18:39 1.2K 
[TXT]Equality.Proposition..>20-Mar-2018 18:39 1.3K 
[TXT]README.html 20-Mar-2018 18:39 1.7K 
[TXT]Agda.Builtin.Equalit..>20-Mar-2018 18:39 2.3K 
[TXT]Agda.Builtin.Bool.html 20-Mar-2018 18:39 2.4K 
[TXT]Agda.Builtin.Size.html 20-Mar-2018 18:39 2.9K 
[TXT]Agda.Builtin.List.html 20-Mar-2018 18:39 3.6K 
[TXT]Agda.Primitive.html 20-Mar-2018 18:39 3.6K 
[TXT]Equality.Proposition..>20-Mar-2018 18:39 13K 
[TXT]Agda.Primitive.Cubic..>20-Mar-2018 18:39 15K 
[TXT]Lens.Non-dependent.html20-Mar-2018 18:39 15K 
[TXT]Injection.html 20-Mar-2018 18:39 17K 
[TXT]Agda.Builtin.Nat.html 20-Mar-2018 18:39 18K 
[TXT]Logical-equivalence...>20-Mar-2018 18:39 20K 
[TXT]Groupoid.html 20-Mar-2018 18:39 22K 
[TXT]H-level.html 20-Mar-2018 18:39 39K 
[TXT]Surjection.html 20-Mar-2018 18:39 48K 
[TXT]Preimage.html 20-Mar-2018 18:39 59K 
[TXT]List.html 20-Mar-2018 18:39 59K 
[TXT]Embedding.html 20-Mar-2018 18:39 61K 
[TXT]Bool.html 20-Mar-2018 18:39 66K 
[TXT]Equality.Decidable-U..>20-Mar-2018 18:39 70K 
[TXT]Interval.html 20-Mar-2018 18:39 75K 
[TXT]Equality.Decision-pr..>20-Mar-2018 18:39 80K 
[TXT]Record.html 20-Mar-2018 18:39 97K 
[TXT]Equality.Groupoid.html 20-Mar-2018 18:39 104K 
[TXT]Monad.html 20-Mar-2018 18:39 107K 
[TXT]Prelude.html 20-Mar-2018 18:39 124K 
[TXT]README.Record-getter..>20-Mar-2018 18:39 132K 
[TXT]Equality.Tactic.html 20-Mar-2018 18:39 143K 
[TXT]Bijection.html 20-Mar-2018 18:39 152K 
[TXT]H-level.Truncation.P..>20-Mar-2018 18:39 198K 
[TXT]Nat.html 20-Mar-2018 18:39 210K 
[TXT]H-level.Closure.html 20-Mar-2018 18:39 294K 
[TXT]Lens.Non-dependent.T..>20-Mar-2018 18:39 493K 
[TXT]H-level.Truncation.html20-Mar-2018 18:39 554K 
[TXT]Univalence-axiom.html 20-Mar-2018 18:39 567K 
[TXT]Lens.Dependent.html 20-Mar-2018 18:39 597K 
[TXT]Equivalence.html 20-Mar-2018 18:39 621K 
[TXT]Lens.Non-dependent.A..>20-Mar-2018 18:39 691K 
[TXT]Equality.html 20-Mar-2018 18:39 826K 
[TXT]Function-universe.html 20-Mar-2018 18:39 1.4M 

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

{-# OPTIONS --without-K #-}

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