Index of /~nad/listings/dependent-lenses

[ICO]NameLast modifiedSizeDescription

[DIR]Parent Directory   -  
[TXT]Agda.Builtin.Bool.html 10-Jan-2020 18:18 3.5K 
[TXT]Agda.Builtin.Cubical..>10-Jan-2020 18:18 62K 
[TXT]Agda.Builtin.Cubical..>10-Jan-2020 18:18 49K 
[TXT]Agda.Builtin.Cubical..>10-Jan-2020 18:18 4.4K 
[TXT]Agda.Builtin.Cubical..>10-Jan-2020 18:18 4.4K 
[TXT]Agda.Builtin.Equalit..>10-Jan-2020 18:18 2.4K 
[TXT]Agda.Builtin.List.html 10-Jan-2020 18:18 5.0K 
[TXT]Agda.Builtin.Nat.html 10-Jan-2020 18:18 23K 
[TXT]Agda.Builtin.Sigma.html10-Jan-2020 18:18 3.2K 
[TXT]Agda.Builtin.Strict...>10-Jan-2020 18:18 4.7K 
[TXT]Agda.Builtin.Unit.html 10-Jan-2020 18:18 1.6K 
[TXT]Agda.Primitive.Cubic..>10-Jan-2020 18:18 18K 
[TXT]Agda.Primitive.html 10-Jan-2020 18:18 3.8K 
[TXT]Agda.css 10-Jan-2020 18:18 1.6K 
[TXT]Algebra.Bundles.html 10-Jan-2020 18:18 138K 
[TXT]Algebra.Core.html 10-Jan-2020 18:18 2.9K 
[TXT]Algebra.Definitions...>10-Jan-2020 18:18 49K 
[TXT]Algebra.FunctionProp..>10-Jan-2020 18:18 5.3K 
[TXT]Algebra.FunctionProp..>10-Jan-2020 18:18 35K 
[TXT]Algebra.FunctionProp..>10-Jan-2020 18:18 108K 
[TXT]Algebra.FunctionProp..>10-Jan-2020 18:18 2.7K 
[TXT]Algebra.Morphism.Def..>10-Jan-2020 18:18 9.5K 
[TXT]Algebra.Morphism.Str..>10-Jan-2020 18:18 29K 
[TXT]Algebra.Morphism.html 10-Jan-2020 18:18 45K 
[TXT]Algebra.Operations.C..>10-Jan-2020 18:18 45K 
[TXT]Algebra.Operations.S..>10-Jan-2020 18:18 29K 
[TXT]Algebra.Properties.A..>10-Jan-2020 18:18 22K 
[TXT]Algebra.Properties.B..>10-Jan-2020 18:18 292K 
[TXT]Algebra.Properties.D..>10-Jan-2020 18:18 37K 
[TXT]Algebra.Properties.G..>10-Jan-2020 18:18 55K 
[TXT]Algebra.Properties.L..>10-Jan-2020 18:18 56K 
[TXT]Algebra.Properties.R..>10-Jan-2020 18:18 31K 
[TXT]Algebra.Properties.S..>10-Jan-2020 18:18 13K 
[TXT]Algebra.Solver.Ring...>10-Jan-2020 18:18 42K 
[TXT]Algebra.Solver.Ring...>10-Jan-2020 18:18 96K 
[TXT]Algebra.Solver.Ring...>10-Jan-2020 18:18 4.1K 
[TXT]Algebra.Solver.Ring...>10-Jan-2020 18:18 295K 
[TXT]Algebra.Structures.html10-Jan-2020 18:18 115K 
[TXT]Algebra.html 10-Jan-2020 18:18 1.7K 
[TXT]Axiom.Extensionality..>10-Jan-2020 18:18 21K 
[TXT]Axiom.UniquenessOfId..>10-Jan-2020 18:18 21K 
[TXT]Bijection.html 10-Jan-2020 18:18 200K 
[TXT]Bool.html 10-Jan-2020 18:18 73K 
[TXT]Category.Applicative..>10-Jan-2020 18:18 46K 
[TXT]Category.Applicative..>10-Jan-2020 18:18 9.9K 
[TXT]Category.Functor.html 10-Jan-2020 18:18 11K 
[TXT]Category.Monad.Index..>10-Jan-2020 18:18 30K 
[TXT]Category.Monad.html 10-Jan-2020 18:18 12K 
[TXT]Data.Bool.Base.html 10-Jan-2020 18:18 12K 
[TXT]Data.Bool.Properties..>10-Jan-2020 18:18 170K 
[TXT]Data.Empty.Irrelevan..>10-Jan-2020 18:18 2.1K 
[TXT]Data.Empty.html 10-Jan-2020 18:18 1.9K 
[TXT]Data.Fin.Base.html 10-Jan-2020 18:18 91K 
[TXT]Data.Fin.Properties...>10-Jan-2020 18:18 284K 
[TXT]Data.Fin.html 10-Jan-2020 18:18 4.5K 
[TXT]Data.List.Base.html 10-Jan-2020 18:18 153K 
[TXT]Data.List.html 10-Jan-2020 18:18 1.3K 
[TXT]Data.Maybe.Base.html 10-Jan-2020 18:18 36K 
[TXT]Data.Nat.Base.html 10-Jan-2020 18:18 49K 
[TXT]Data.Nat.Properties...>10-Jan-2020 18:18 821K 
[TXT]Data.Nat.Solver.html 10-Jan-2020 18:18 2.7K 
[TXT]Data.Nat.html 10-Jan-2020 18:18 3.9K 
[TXT]Data.Product.html 10-Jan-2020 18:18 57K 
[TXT]Data.Sum.Base.html 10-Jan-2020 18:18 25K 
[TXT]Data.Sum.html 10-Jan-2020 18:18 11K 
[TXT]Data.Table.Base.html 10-Jan-2020 18:18 29K 
[TXT]Data.These.Base.html 10-Jan-2020 18:18 36K 
[TXT]Data.Unit.Base.html 10-Jan-2020 18:18 3.2K 
[TXT]Data.Unit.Properties..>10-Jan-2020 18:18 27K 
[TXT]Data.Unit.html 10-Jan-2020 18:18 5.7K 
[TXT]Data.Vec.Base.html 10-Jan-2020 18:18 135K 
[TXT]Data.Vec.Bounded.Bas..>10-Jan-2020 18:18 30K 
[TXT]Data.Vec.N-ary.html 10-Jan-2020 18:18 81K 
[TXT]Data.Vec.html 10-Jan-2020 18:18 12K 
[TXT]Embedding.html 10-Jan-2020 18:18 63K 
[TXT]Equality.Decidable-U..>10-Jan-2020 18:18 68K 
[TXT]Equality.Decision-pr..>10-Jan-2020 18:18 84K 
[TXT]Equality.Groupoid.html 10-Jan-2020 18:18 100K 
[TXT]Equality.Instances-r..>10-Jan-2020 18:18 121K 
[TXT]Equality.Path.Isomor..>10-Jan-2020 18:18 245K 
[TXT]Equality.Path.html 10-Jan-2020 18:18 272K 
[TXT]Equality.Proposition..>10-Jan-2020 18:18 15K 
[TXT]Equality.Tactic.html 10-Jan-2020 18:18 144K 
[TXT]Equality.html 10-Jan-2020 18:18 955K 
[TXT]Equivalence.html 10-Jan-2020 18:18 632K 
[TXT]Function-universe.html 10-Jan-2020 18:18 1.7M 
[TXT]Function.Base.html 10-Jan-2020 18:18 46K 
[TXT]Function.Bundles.html 10-Jan-2020 18:18 75K 
[TXT]Function.Core.html 10-Jan-2020 18:18 2.9K 
[TXT]Function.Definitions..>10-Jan-2020 18:18 5.0K 
[TXT]Function.Definitions..>10-Jan-2020 18:18 7.7K 
[TXT]Function.Definitions..>10-Jan-2020 18:18 13K 
[TXT]Function.Equality.html 10-Jan-2020 18:18 39K 
[TXT]Function.Equivalence..>10-Jan-2020 18:18 39K 
[TXT]Function.Injection.html10-Jan-2020 18:18 22K 
[TXT]Function.Structures...>10-Jan-2020 18:18 28K 
[TXT]Function.html 10-Jan-2020 18:18 1.8K 
[TXT]Groupoid.html 10-Jan-2020 18:18 46K 
[TXT]H-level.Closure.html 10-Jan-2020 18:18 329K 
[TXT]H-level.Truncation.C..>10-Jan-2020 18:18 582K 
[TXT]H-level.Truncation.P..>10-Jan-2020 18:18 207K 
[TXT]H-level.html 10-Jan-2020 18:18 52K 
[TXT]Injection.html 10-Jan-2020 18:18 17K 
[TXT]Lens.Dependent.html 10-Jan-2020 18:18 598K 
[TXT]Lens.Non-dependent.A..>10-Jan-2020 18:18 701K 
[TXT]Lens.Non-dependent.T..>10-Jan-2020 18:19 497K 
[TXT]Lens.Non-dependent.html10-Jan-2020 18:18 16K 
[TXT]Level.html 10-Jan-2020 18:19 5.5K 
[TXT]List.html 10-Jan-2020 18:19 270K 
[TXT]Logical-equivalence...>10-Jan-2020 18:19 22K 
[TXT]Monad.html 10-Jan-2020 18:19 129K 
[TXT]Nat.Solver.html 10-Jan-2020 18:19 60K 
[TXT]Nat.html 10-Jan-2020 18:19 421K 
[TXT]Pointed-type.html 10-Jan-2020 18:19 79K 
[TXT]Preimage.html 10-Jan-2020 18:19 59K 
[TXT]Prelude.html 10-Jan-2020 18:19 125K 
[TXT]README.Record-getter..>10-Jan-2020 18:19 135K 
[TXT]README.html 10-Jan-2020 18:19 1.7K 
[TXT]Records-with-with.html 10-Jan-2020 18:19 107K 
[TXT]Relation.Binary.Bund..>10-Jan-2020 18:19 51K 
[TXT]Relation.Binary.Cons..>10-Jan-2020 18:19 70K 
[TXT]Relation.Binary.Cons..>10-Jan-2020 18:19 77K 
[TXT]Relation.Binary.Cons..>10-Jan-2020 18:19 71K 
[TXT]Relation.Binary.Core..>10-Jan-2020 18:19 17K 
[TXT]Relation.Binary.Defi..>10-Jan-2020 18:19 66K 
[TXT]Relation.Binary.Inde..>10-Jan-2020 18:19 11K 
[TXT]Relation.Binary.Inde..>10-Jan-2020 18:19 16K 
[TXT]Relation.Binary.Inde..>10-Jan-2020 18:19 13K 
[TXT]Relation.Binary.Inde..>10-Jan-2020 18:19 10K 
[TXT]Relation.Binary.Inde..>10-Jan-2020 18:19 13K 
[TXT]Relation.Binary.Inde..>10-Jan-2020 18:19 4.6K 
[TXT]Relation.Binary.Latt..>10-Jan-2020 18:19 141K 
[TXT]Relation.Binary.Morp..>10-Jan-2020 18:19 6.4K 
[TXT]Relation.Binary.Morp..>10-Jan-2020 18:19 37K 
[TXT]Relation.Binary.Prop..>10-Jan-2020 18:19 21K 
[TXT]Relation.Binary.Prop..>10-Jan-2020 18:19 8.3K 
[TXT]Relation.Binary.Prop..>10-Jan-2020 18:19 37K 
[TXT]Relation.Binary.Prop..>10-Jan-2020 18:19 110K 
[TXT]Relation.Binary.Reas..>10-Jan-2020 18:19 17K 
[TXT]Relation.Binary.Reas..>10-Jan-2020 18:19 4.6K 
[TXT]Relation.Binary.Reas..>10-Jan-2020 18:19 66K 
[TXT]Relation.Binary.Reas..>10-Jan-2020 18:19 5.4K 
[TXT]Relation.Binary.Reas..>10-Jan-2020 18:19 7.9K 
[TXT]Relation.Binary.Refl..>10-Jan-2020 18:19 36K 
[TXT]Relation.Binary.Stru..>10-Jan-2020 18:19 52K 
[TXT]Relation.Binary.html 10-Jan-2020 18:19 1.9K 
[TXT]Relation.Nullary.Dec..>10-Jan-2020 18:19 42K 
[TXT]Relation.Nullary.Dec..>10-Jan-2020 18:19 12K 
[TXT]Relation.Nullary.Neg..>10-Jan-2020 18:19 59K 
[TXT]Relation.Nullary.Pro..>10-Jan-2020 18:19 9.3K 
[TXT]Relation.Nullary.Ref..>10-Jan-2020 18:19 11K 
[TXT]Relation.Nullary.Sum..>10-Jan-2020 18:19 10K 
[TXT]Relation.Nullary.html 10-Jan-2020 18:19 13K 
[TXT]Relation.Unary.Prope..>10-Jan-2020 18:19 35K 
[TXT]Relation.Unary.html 10-Jan-2020 18:19 84K 
[TXT]Strict.html 10-Jan-2020 18:19 6.9K 
[TXT]Surjection.html 10-Jan-2020 18:19 87K 
[TXT]Univalence-axiom.html 10-Jan-2020 18:19 637K 

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