Index of /~nad/listings/dependent-lenses

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Univalence-axiom.html 17-Oct-2017 22:41 565K 
[TXT]Surjection.html 17-Oct-2017 22:41 50K 
[TXT]Record.html 17-Oct-2017 22:41 96K 
[TXT]README.html 17-Oct-2017 22:41 1.7K 
[TXT]README.Record-getter..>17-Oct-2017 22:41 131K 
[TXT]Prelude.html 17-Oct-2017 22:41 124K 
[TXT]Preimage.html 17-Oct-2017 22:41 59K 
[TXT]Nat.html 17-Oct-2017 22:41 84K 
[TXT]Monad.html 17-Oct-2017 22:41 124K 
[TXT]Logical-equivalence...>17-Oct-2017 22:41 20K 
[TXT]List.html 17-Oct-2017 22:41 59K 
[TXT]Lens.Non-dependent.html17-Oct-2017 22:41 15K 
[TXT]Lens.Non-dependent.T..>17-Oct-2017 22:41 493K 
[TXT]Lens.Non-dependent.A..>17-Oct-2017 22:41 688K 
[TXT]Lens.Dependent.html 17-Oct-2017 22:41 594K 
[TXT]Interval.html 17-Oct-2017 22:41 74K 
[TXT]Injection.html 17-Oct-2017 22:41 17K 
[TXT]H-level.html 17-Oct-2017 22:41 38K 
[TXT]H-level.Truncation.html17-Oct-2017 22:41 552K 
[TXT]H-level.Truncation.P..>17-Oct-2017 22:41 197K 
[TXT]H-level.Closure.html 17-Oct-2017 22:41 292K 
[TXT]Groupoid.html 17-Oct-2017 22:41 45K 
[TXT]Function-universe.html 17-Oct-2017 22:41 1.4M 
[TXT]Equivalence.html 17-Oct-2017 22:41 647K 
[TXT]Equality.html 17-Oct-2017 22:41 819K 
[TXT]Equality.Tactic.html 17-Oct-2017 22:41 143K 
[TXT]Equality.Proposition..>17-Oct-2017 22:41 13K 
[TXT]Equality.Proposition..>17-Oct-2017 22:41 1.3K 
[TXT]Equality.Groupoid.html 17-Oct-2017 22:41 104K 
[TXT]Equality.Decision-pr..>17-Oct-2017 22:41 78K 
[TXT]Equality.Decidable-U..>17-Oct-2017 22:41 70K 
[TXT]Embedding.html 17-Oct-2017 22:41 62K 
[TXT]Bool.html 17-Oct-2017 22:41 66K 
[TXT]Bijection.html 17-Oct-2017 22:41 156K 
[TXT]Agda.css 17-Oct-2017 22:41 1.2K 
[TXT]Agda.Primitive.html 17-Oct-2017 22:41 3.6K 
[TXT]Agda.Primitive.Cubic..>17-Oct-2017 22:41 14K 
[TXT]Agda.Builtin.Unit.html 17-Oct-2017 22:41 1.2K 
[TXT]Agda.Builtin.Size.html 17-Oct-2017 22:41 1.6K 
[TXT]Agda.Builtin.Nat.html 17-Oct-2017 22:41 17K 
[TXT]Agda.Builtin.List.html 17-Oct-2017 22:41 4.2K 
[TXT]Agda.Builtin.Equalit..>17-Oct-2017 22:41 2.2K 
[TXT]Agda.Builtin.Bool.html 17-Oct-2017 22:41 2.4K 

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