pijul nest
guest › [sign in] [explore]
{/} code [~] changes [>] discussions [*] jobs

Fork channel

Create a new channel as a copy of main.

Rename channel

Rename main to:

Delete channel

Delete main? This cannot be undone.
tzemanovic
10. Lists
Created by tzemanovic on Feb 26, 2026, 10:34 AM
634YGOQIKLAS2II5EAPSFDLZAR2CM3YBIJIO46M5OJ6JKXRZRDJQC
State: TWA4NN6RBHY3Y37HVR7GQ4LKURIVIDY37ZNGXBRJRLXPMLVM3RWAC
  • standard-library/src/Data/List.agda
  • standard-library/src/Data/List/Properties.agda
  • standard-library/src/Data/Fin/Properties.agda
  • src/plfa/part1/Lists.lagda.md
tzemanovic
9. Decidable
Created by tzemanovic on Feb 22, 2026, 3:09 PM
3XE75GH6ZU5V43D5GQTZ36RSTJMEKXMRR6PWLWSC5Q4VOCIW6P4AC
State: XCPSCII2HQPAWDRUPPDXTEF6DANJECY6LNL3MS6XD2FKUXZAMQVQC
  • src/plfa/part1/Decidable.lagda.md
tzemanovic
proof postulates in quantifiers
Created by tzemanovic on Feb 20, 2026, 1:48 PM
AIYDIDGHASF7RY62YUGLYIRE7PGNR3CJJFNJQZV2LRRP76VCA5WQC
State: 3KHE4QZNY5XDN2LBEZN6TUKE4KBFFWTKEKVILNW7ME7Z6MJC5X5QC
  • src/plfa/part1/Quantifiers.lagda.md
tzemanovic
8. Quantifiers
Created by tzemanovic on Feb 19, 2026, 2:48 PM
FHLV6O6R4Q43SMIT2VWPRZA6EMOL4N6X5A4UO56NQDPBFUPQ4T6AC
State: 2UAMGBDBUV7GL52THPZGLYQQ4VAFKKRILS4DFYC3NJL2NQ75GDZQC
  • src/plfa/part1/Relations.lagda.md
  • src/plfa/part1/Quantifiers.lagda.md
tzemanovic
7. Negation
Created by tzemanovic on Feb 17, 2026, 2:31 PM
T5OZLUEU6FUYDNWCXEGRUEG5PC6SM4GKPF7JBR4RMLFW23437WLAC
State: 6WQJMLV2SYOL7OED3KYR6U4HAUD2QL3YMQ3F3DPJEOBGTXKJ63RAC
  • src/plfa/part1/Negation.lagda.md
tzemanovic
6. Connectives
Created by tzemanovic on Feb 15, 2026, 4:38 PM
7U7RBTIPOZJMUFMW6OKAC7BNHTW53JKYWZP2IRICHAYDOPNKXJMAC
State: GS3Z7MHYWBHAUXA6YT46S4ZBRSMOD7VE3ZJ57HTC4PORP574GXPAC
  • src/plfa/part1/Connectives.lagda.md
tzemanovic
fix notation
Created by tzemanovic on Feb 15, 2026, 11:31 AM
NM2NNVP2JD5JHHUGZIDMKOD3MNQPDV2JF4IHO65SCSDMNYUPWPIAC
State: 6EAB36DSBBWTXQL2MHPW7GIP3MMZ4JMVLJVWCPDTC4R7HBC265WQC
  • src/plfa/part1/Isomorphism.lagda.md
tzemanovic
style
Created by tzemanovic on Feb 13, 2026, 4:09 PM
DCMGBGUTZJXO6RF6DMSTUZOG3GG5QQTIIEYUY5RZSKTHUN2GP6UAC
State: RZVKOG262CQTVZ2GPAYLGO3PKGVHIZGSLQG7OI77KXFZMXU55MNAC
  • src/plfa/part1/Isomorphism.lagda.md
tzemanovic
simplify isomorphism exercise with an import
Created by tzemanovic on Feb 13, 2026, 4:06 PM
ZKA4IYXCTK6QCBUQPQ3N5AVNEM5O7OZTNF2JY2GG3GNHP6GTVTGAC
State: 6RNJ2AU62652QLSRH345THYUGWZRG3YBMIP3IIC25BSXK4ZJDTOQC
  • src/plfa/part1/Isomorphism.lagda.md
tzemanovic
5. Isomorphism
Created by tzemanovic on Feb 13, 2026, 3:59 PM
4GFM7RKRTS44QVOSYDD7U7ANWPOPTJJ55Y6X4BJLQJAZ3Y6XLOKQC
State: YXJ7OC2VI7SUIBVIZ2OT6APADQKPESEOCWXQO4QN35VEWZR3PO3AC
  • src/plfa/part1/Isomorphism.lagda.md
tzemanovic
ignore /src/_build
Created by tzemanovic on Feb 13, 2026, 1:01 PM
FUXV43PVZVTXQHIERAF2BDBCXUFW2AKPFDJTGEKFIOBGRIHVFXHAC
State: R23PT4RCJKYATABIBYLF2S2ZIPMRCA5BFZPB33ZQB5TCVH32YSZQC
  • .ignore
tzemanovic
update .ignore
Created by tzemanovic on Feb 13, 2026, 1:00 PM
KP5GBJVKNNXJSXXNDN774RRQCCH3PWX5XY7S66IBZQRF2X2YDANQC
State: ZHPJ5FFI5T6DN7L7EVD7HWSCQLDN36VFA2C6ZFJPJWR3HNU4HAEAC
  • standard-library/.ignore
  • .ignore
tzemanovic
add standard-library
Created by tzemanovic on Feb 13, 2026, 12:59 PM
GP7YEIGGU3IPEBURKAKH5SIXYRVFYZILAQRSUDU3FDFI2G66HOQQC
State: 2DUJXYJHXRKZPVYNMTL3IL72SMABKQT4GIIIA4ATGPILQY6WXRYQC
  • standard-library
  • standard-library/tests
  • standard-library/tests/text
  • standard-library/tests/text/tabular
  • standard-library/tests/text/tabular/tabular.agda-lib
  • standard-library/tests/text/tabular/run
  • standard-library/tests/text/tabular/expected
  • standard-library/tests/text/tabular/Main.agda
1847 more files
  • standard-library/tests/text/regex
  • standard-library/tests/text/regex/run
  • standard-library/tests/text/regex/regex.agda-lib
  • standard-library/tests/text/regex/expected
  • standard-library/tests/text/regex/Main.agda
  • standard-library/tests/text/printf
  • standard-library/tests/text/printf/run
  • standard-library/tests/text/printf/printf.agda-lib
  • standard-library/tests/text/printf/expected
  • standard-library/tests/text/printf/Main.agda
  • standard-library/tests/text/pretty
  • standard-library/tests/text/pretty/run
  • standard-library/tests/text/pretty/pretty.agda-lib
  • standard-library/tests/text/pretty/expected
  • standard-library/tests/text/pretty/Main.agda
  • standard-library/tests/system
  • standard-library/tests/system/random
  • standard-library/tests/system/random/run
  • standard-library/tests/system/random/random.agda-lib
  • standard-library/tests/system/random/expected
  • standard-library/tests/system/random/Main.agda
  • standard-library/tests/system/random/.gitignore
  • standard-library/tests/system/io
  • standard-library/tests/system/io/run
  • standard-library/tests/system/io/io.agda-lib
  • standard-library/tests/system/io/input
  • standard-library/tests/system/io/expected
  • standard-library/tests/system/io/Main.agda
  • standard-library/tests/system/environment
  • standard-library/tests/system/environment/run
  • standard-library/tests/system/environment/expected
  • standard-library/tests/system/environment/environment.agda-lib
  • standard-library/tests/system/environment/Main.agda
  • standard-library/tests/system/directory
  • standard-library/tests/system/directory/run
  • standard-library/tests/system/directory/expected
  • standard-library/tests/system/directory/directory.agda-lib
  • standard-library/tests/system/directory/Main.agda
  • standard-library/tests/system/ansi
  • standard-library/tests/system/ansi/run
  • standard-library/tests/system/ansi/expected
  • standard-library/tests/system/ansi/ansi.agda-lib
  • standard-library/tests/system/ansi/Main.agda
  • standard-library/tests/standard-library-tests.agda-lib
  • standard-library/tests/show
  • standard-library/tests/show/tree
  • standard-library/tests/show/tree/tree.agda-lib
  • standard-library/tests/show/tree/run
  • standard-library/tests/show/tree/expected
  • standard-library/tests/show/tree/Main.agda
  • standard-library/tests/show/reflection
  • standard-library/tests/show/reflection/run
  • standard-library/tests/show/reflection/reflection.agda-lib
  • standard-library/tests/show/reflection/expected
  • standard-library/tests/show/reflection/Main.agda
  • standard-library/tests/show/num
  • standard-library/tests/show/num/run
  • standard-library/tests/show/num/num.agda-lib
  • standard-library/tests/show/num/expected
  • standard-library/tests/show/num/Main.agda
  • standard-library/tests/runtests.agda
  • standard-library/tests/reflection
  • standard-library/tests/reflection/assumption
  • standard-library/tests/reflection/assumption/run
  • standard-library/tests/reflection/assumption/expected
  • standard-library/tests/reflection/assumption/assumption.agda-lib
  • standard-library/tests/reflection/assumption/Main.agda
  • standard-library/tests/monad
  • standard-library/tests/monad/tcm
  • standard-library/tests/monad/tcm/tcm.agda-lib
  • standard-library/tests/monad/tcm/run
  • standard-library/tests/monad/tcm/expected
  • standard-library/tests/monad/tcm/Main.agda
  • standard-library/tests/monad/pythagorean
  • standard-library/tests/monad/pythagorean/run
  • standard-library/tests/monad/pythagorean/pythagorean.agda-lib
  • standard-library/tests/monad/pythagorean/expected
  • standard-library/tests/monad/pythagorean/Main.agda
  • standard-library/tests/monad/fibonacci
  • standard-library/tests/monad/fibonacci/run
  • standard-library/tests/monad/fibonacci/fibonacci.agda-lib
  • standard-library/tests/monad/fibonacci/expected
  • standard-library/tests/monad/fibonacci/Main.agda
  • standard-library/tests/monad/counting
  • standard-library/tests/monad/counting/run
  • standard-library/tests/monad/counting/expected
  • standard-library/tests/monad/counting/counting.agda-lib
  • standard-library/tests/monad/counting/Main.agda
  • standard-library/tests/data
  • standard-library/tests/data/trie
  • standard-library/tests/data/trie/trie.agda-lib
  • standard-library/tests/data/trie/run
  • standard-library/tests/data/trie/expected
  • standard-library/tests/data/trie/Main.agda
  • standard-library/tests/data/rational-unnormalised
  • standard-library/tests/data/rational-unnormalised/run
  • standard-library/tests/data/rational-unnormalised/rational-unnormalised.agda-lib
  • standard-library/tests/data/rational-unnormalised/expected
  • standard-library/tests/data/rational-unnormalised/Main.agda
  • standard-library/tests/data/rational
  • standard-library/tests/data/rational/run
  • standard-library/tests/data/rational/rational.agda-lib
  • standard-library/tests/data/rational/expected
  • standard-library/tests/data/rational/Main.agda
  • standard-library/tests/data/list
  • standard-library/tests/data/list/run
  • standard-library/tests/data/list/list.agda-lib
  • standard-library/tests/data/list/expected
  • standard-library/tests/data/list/Main.agda
  • standard-library/tests/data/colist
  • standard-library/tests/data/colist/run
  • standard-library/tests/data/colist/expected
  • standard-library/tests/data/colist/colist.agda-lib
  • standard-library/tests/data/colist/Main.agda
  • standard-library/tests/data/bytestring
  • standard-library/tests/data/bytestring/run
  • standard-library/tests/data/bytestring/expected
  • standard-library/tests/data/bytestring/bytestring.agda-lib
  • standard-library/tests/data/bytestring/Main.agda
  • standard-library/tests/data/appending
  • standard-library/tests/data/appending/run
  • standard-library/tests/data/appending/input
  • standard-library/tests/data/appending/expected
  • standard-library/tests/data/appending/appending.agda-lib
  • standard-library/tests/data/appending/TakeWhile.agda
  • standard-library/tests/data/appending/Main.agda
  • standard-library/tests/Makefile
  • standard-library/standard-library.agda-lib
  • standard-library/stack-9.6.2.yaml
  • standard-library/stack-9.4.5.yaml
  • standard-library/stack-9.2.8.yaml
  • standard-library/stack-9.0.2.yaml
  • standard-library/stack-8.8.4.yaml
  • standard-library/stack-8.8.3.yaml
  • standard-library/stack-8.8.2.yaml
  • standard-library/stack-8.6.5.yaml
  • standard-library/stack-8.4.4.yaml
  • standard-library/stack-8.2.2.yaml
  • standard-library/stack-8.10.7.yaml
  • standard-library/stack-8.10.5.yaml
  • standard-library/stack-8.0.2.yaml
  • standard-library/src
  • standard-library/src/Text
  • standard-library/src/Text/Tree
  • standard-library/src/Text/Tree/Linear.agda
  • standard-library/src/Text/Tabular
  • standard-library/src/Text/Tabular/Vec.agda
  • standard-library/src/Text/Tabular/List.agda
  • standard-library/src/Text/Tabular/Base.agda
  • standard-library/src/Text/Regex.agda
  • standard-library/src/Text/Regex
  • standard-library/src/Text/Regex/String.agda
  • standard-library/src/Text/Regex/String
  • standard-library/src/Text/Regex/String/Unsafe.agda
  • standard-library/src/Text/Regex/SmartConstructors.agda
  • standard-library/src/Text/Regex/Search.agda
  • standard-library/src/Text/Regex/Properties.agda
  • standard-library/src/Text/Regex/Properties
  • standard-library/src/Text/Regex/Properties/Core.agda
  • standard-library/src/Text/Regex/Derivative
  • standard-library/src/Text/Regex/Derivative/Brzozowski.agda
  • standard-library/src/Text/Regex/Base.agda
  • standard-library/src/Text/Printf.agda
  • standard-library/src/Text/Printf
  • standard-library/src/Text/Printf/Generic.agda
  • standard-library/src/Text/Pretty.agda
  • standard-library/src/Text/Pretty
  • standard-library/src/Text/Pretty/Core.agda
  • standard-library/src/Text/Format.agda
  • standard-library/src/Text/Format
  • standard-library/src/Text/Format/Generic.agda
  • standard-library/src/Test
  • standard-library/src/Test/Golden.agda
  • standard-library/src/Tactic
  • standard-library/src/Tactic/RingSolver.agda
  • standard-library/src/Tactic/RingSolver
  • standard-library/src/Tactic/RingSolver/NonReflective.agda
  • standard-library/src/Tactic/RingSolver/Core
  • standard-library/src/Tactic/RingSolver/Core/Polynomial
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Semantics.agda
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Reasoning.agda
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Parameters.agda
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Homomorphism.agda
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Homomorphism
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Variables.agda
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Negation.agda
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Multiplication.agda
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Lemmas.agda
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Exponentiation.agda
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Constants.agda
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Homomorphism/Addition.agda
  • standard-library/src/Tactic/RingSolver/Core/Polynomial/Base.agda
  • standard-library/src/Tactic/RingSolver/Core/NatSet.agda
  • standard-library/src/Tactic/RingSolver/Core/Expression.agda
  • standard-library/src/Tactic/RingSolver/Core/AlmostCommutativeRing.agda
  • standard-library/src/Tactic/MonoidSolver.agda
  • standard-library/src/Tactic/Cong.agda
  • standard-library/src/System
  • standard-library/src/System/Random.agda
  • standard-library/src/System/Random
  • standard-library/src/System/Random/Primitive.agda
  • standard-library/src/System/Process.agda
  • standard-library/src/System/Process
  • standard-library/src/System/Process/Primitive.agda
  • standard-library/src/System/FilePath
  • standard-library/src/System/FilePath/Posix.agda
  • standard-library/src/System/FilePath/Posix
  • standard-library/src/System/FilePath/Posix/Primitive.agda
  • standard-library/src/System/Exit.agda
  • standard-library/src/System/Exit
  • standard-library/src/System/Exit/Primitive.agda
  • standard-library/src/System/Environment.agda
  • standard-library/src/System/Environment
  • standard-library/src/System/Environment/Primitive.agda
  • standard-library/src/System/Directory.agda
  • standard-library/src/System/Directory
  • standard-library/src/System/Directory/Primitive.agda
  • standard-library/src/System/Console
  • standard-library/src/System/Console/ANSI.agda
  • standard-library/src/System/Clock.agda
  • standard-library/src/System/Clock
  • standard-library/src/System/Clock/Primitive.agda
  • standard-library/src/Strict.agda
  • standard-library/src/Size.agda
  • standard-library/src/Relation
  • standard-library/src/Relation/Unary.agda
  • standard-library/src/Relation/Unary
  • standard-library/src/Relation/Unary/Sized.agda
  • standard-library/src/Relation/Unary/Relation
  • standard-library/src/Relation/Unary/Relation/Binary
  • standard-library/src/Relation/Unary/Relation/Binary/Subset.agda
  • standard-library/src/Relation/Unary/Relation/Binary/Equality.agda
  • standard-library/src/Relation/Unary/Properties.agda
  • standard-library/src/Relation/Unary/PredicateTransformer.agda
  • standard-library/src/Relation/Unary/Polymorphic.agda
  • standard-library/src/Relation/Unary/Polymorphic
  • standard-library/src/Relation/Unary/Polymorphic/Properties.agda
  • standard-library/src/Relation/Unary/Indexed.agda
  • standard-library/src/Relation/Unary/Consequences.agda
  • standard-library/src/Relation/Unary/Closure
  • standard-library/src/Relation/Unary/Closure/StrictPartialOrder.agda
  • standard-library/src/Relation/Unary/Closure/Preorder.agda
  • standard-library/src/Relation/Unary/Closure/Base.agda
  • standard-library/src/Relation/Unary/Algebra.agda
  • standard-library/src/Relation/Nullary.agda
  • standard-library/src/Relation/Nullary
  • standard-library/src/Relation/Nullary/Universe.agda
  • standard-library/src/Relation/Nullary/Sum.agda
  • standard-library/src/Relation/Nullary/Reflects.agda
  • standard-library/src/Relation/Nullary/Recomputable.agda
  • standard-library/src/Relation/Nullary/Product.agda
  • standard-library/src/Relation/Nullary/Negation.agda
  • standard-library/src/Relation/Nullary/Negation
  • standard-library/src/Relation/Nullary/Negation/Core.agda
  • standard-library/src/Relation/Nullary/Indexed.agda
  • standard-library/src/Relation/Nullary/Indexed
  • standard-library/src/Relation/Nullary/Indexed/Negation.agda
  • standard-library/src/Relation/Nullary/Implication.agda
  • standard-library/src/Relation/Nullary/Decidable.agda
  • standard-library/src/Relation/Nullary/Decidable
  • standard-library/src/Relation/Nullary/Decidable/Core.agda
  • standard-library/src/Relation/Nullary/Construct
  • standard-library/src/Relation/Nullary/Construct/Add
  • standard-library/src/Relation/Nullary/Construct/Add/Supremum.agda
  • standard-library/src/Relation/Nullary/Construct/Add/Point.agda
  • standard-library/src/Relation/Nullary/Construct/Add/Infimum.agda
  • standard-library/src/Relation/Nullary/Construct/Add/Extrema.agda
  • standard-library/src/Relation/Nary.agda
  • standard-library/src/Relation/Binary.agda
  • standard-library/src/Relation/Binary
  • standard-library/src/Relation/Binary/TypeClasses.agda
  • standard-library/src/Relation/Binary/Structures.agda
  • standard-library/src/Relation/Binary/Structures
  • standard-library/src/Relation/Binary/Structures/Biased.agda
  • standard-library/src/Relation/Binary/Rewriting.agda
  • standard-library/src/Relation/Binary/Reflection.agda
  • standard-library/src/Relation/Binary/Reasoning
  • standard-library/src/Relation/Binary/Reasoning/Syntax.agda
  • standard-library/src/Relation/Binary/Reasoning/StrictPartialOrder.agda
  • standard-library/src/Relation/Binary/Reasoning/Setoid.agda
  • standard-library/src/Relation/Binary/Reasoning/Preorder.agda
  • standard-library/src/Relation/Binary/Reasoning/PartialSetoid.agda
  • standard-library/src/Relation/Binary/Reasoning/PartialOrder.agda
  • standard-library/src/Relation/Binary/Reasoning/MultiSetoid.agda
  • standard-library/src/Relation/Binary/Reasoning/Base
  • standard-library/src/Relation/Binary/Reasoning/Base/Triple.agda
  • standard-library/src/Relation/Binary/Reasoning/Base/Single.agda
  • standard-library/src/Relation/Binary/Reasoning/Base/Partial.agda
  • standard-library/src/Relation/Binary/Reasoning/Base/Double.agda
  • standard-library/src/Relation/Binary/Reasoning/Base/Apartness.agda
  • standard-library/src/Relation/Binary/PropositionalEquality.agda
  • standard-library/src/Relation/Binary/PropositionalEquality
  • standard-library/src/Relation/Binary/PropositionalEquality/WithK.agda
  • standard-library/src/Relation/Binary/PropositionalEquality/TrustMe.agda
  • standard-library/src/Relation/Binary/PropositionalEquality/Properties.agda
  • standard-library/src/Relation/Binary/PropositionalEquality/Core.agda
  • standard-library/src/Relation/Binary/PropositionalEquality/Algebra.agda
  • standard-library/src/Relation/Binary/Properties
  • standard-library/src/Relation/Binary/Properties/TotalOrder.agda
  • standard-library/src/Relation/Binary/Properties/StrictTotalOrder.agda
  • standard-library/src/Relation/Binary/Properties/StrictPartialOrder.agda
  • standard-library/src/Relation/Binary/Properties/Setoid.agda
  • standard-library/src/Relation/Binary/Properties/Preorder.agda
  • standard-library/src/Relation/Binary/Properties/Poset.agda
  • standard-library/src/Relation/Binary/Properties/MeetSemilattice.agda
  • standard-library/src/Relation/Binary/Properties/Lattice.agda
  • standard-library/src/Relation/Binary/Properties/JoinSemilattice.agda
  • standard-library/src/Relation/Binary/Properties/HeytingAlgebra.agda
  • standard-library/src/Relation/Binary/Properties/DistributiveLattice.agda
  • standard-library/src/Relation/Binary/Properties/DecTotalOrder.agda
  • standard-library/src/Relation/Binary/Properties/DecSetoid.agda
  • standard-library/src/Relation/Binary/Properties/BoundedMeetSemilattice.agda
  • standard-library/src/Relation/Binary/Properties/BoundedLattice.agda
  • standard-library/src/Relation/Binary/Properties/BoundedJoinSemilattice.agda
  • standard-library/src/Relation/Binary/Properties/ApartnessRelation.agda
  • standard-library/src/Relation/Binary/OrderMorphism.agda
  • standard-library/src/Relation/Binary/Morphism.agda
  • standard-library/src/Relation/Binary/Morphism
  • standard-library/src/Relation/Binary/Morphism/Structures.agda
  • standard-library/src/Relation/Binary/Morphism/RelMonomorphism.agda
  • standard-library/src/Relation/Binary/Morphism/OrderMonomorphism.agda
  • standard-library/src/Relation/Binary/Morphism/Definitions.agda
  • standard-library/src/Relation/Binary/Morphism/Construct
  • standard-library/src/Relation/Binary/Morphism/Construct/Identity.agda
  • standard-library/src/Relation/Binary/Morphism/Construct/Constant.agda
  • standard-library/src/Relation/Binary/Morphism/Construct/Composition.agda
  • standard-library/src/Relation/Binary/Morphism/Bundles.agda
  • standard-library/src/Relation/Binary/Lattice.agda
  • standard-library/src/Relation/Binary/Lattice
  • standard-library/src/Relation/Binary/Lattice/Structures.agda
  • standard-library/src/Relation/Binary/Lattice/Properties
  • standard-library/src/Relation/Binary/Lattice/Properties/MeetSemilattice.agda
  • standard-library/src/Relation/Binary/Lattice/Properties/Lattice.agda
  • standard-library/src/Relation/Binary/Lattice/Properties/JoinSemilattice.agda
  • standard-library/src/Relation/Binary/Lattice/Properties/HeytingAlgebra.agda
  • standard-library/src/Relation/Binary/Lattice/Properties/DistributiveLattice.agda
  • standard-library/src/Relation/Binary/Lattice/Properties/BoundedMeetSemilattice.agda
  • standard-library/src/Relation/Binary/Lattice/Properties/BoundedLattice.agda
  • standard-library/src/Relation/Binary/Lattice/Properties/BoundedJoinSemilattice.agda
  • standard-library/src/Relation/Binary/Lattice/Definitions.agda
  • standard-library/src/Relation/Binary/Lattice/Bundles.agda
  • standard-library/src/Relation/Binary/Indexed
  • standard-library/src/Relation/Binary/Indexed/Homogeneous.agda
  • standard-library/src/Relation/Binary/Indexed/Homogeneous
  • standard-library/src/Relation/Binary/Indexed/Homogeneous/Structures.agda
  • standard-library/src/Relation/Binary/Indexed/Homogeneous/Definitions.agda
  • standard-library/src/Relation/Binary/Indexed/Homogeneous/Core.agda
  • standard-library/src/Relation/Binary/Indexed/Homogeneous/Construct
  • standard-library/src/Relation/Binary/Indexed/Homogeneous/Construct/At.agda
  • standard-library/src/Relation/Binary/Indexed/Homogeneous/Bundles.agda
  • standard-library/src/Relation/Binary/Indexed/Heterogeneous.agda
  • standard-library/src/Relation/Binary/Indexed/Heterogeneous
  • standard-library/src/Relation/Binary/Indexed/Heterogeneous/Structures.agda
  • standard-library/src/Relation/Binary/Indexed/Heterogeneous/Definitions.agda
  • standard-library/src/Relation/Binary/Indexed/Heterogeneous/Core.agda
  • standard-library/src/Relation/Binary/Indexed/Heterogeneous/Construct
  • standard-library/src/Relation/Binary/Indexed/Heterogeneous/Construct/Trivial.agda
  • standard-library/src/Relation/Binary/Indexed/Heterogeneous/Construct/At.agda
  • standard-library/src/Relation/Binary/Indexed/Heterogeneous/Bundles.agda
  • standard-library/src/Relation/Binary/HeterogeneousEquality.agda
  • standard-library/src/Relation/Binary/HeterogeneousEquality
  • standard-library/src/Relation/Binary/HeterogeneousEquality/Quotients.agda
  • standard-library/src/Relation/Binary/HeterogeneousEquality/Quotients
  • standard-library/src/Relation/Binary/HeterogeneousEquality/Quotients/Examples.agda
  • standard-library/src/Relation/Binary/HeterogeneousEquality/Core.agda
  • standard-library/src/Relation/Binary/Definitions.agda
  • standard-library/src/Relation/Binary/Core.agda
  • standard-library/src/Relation/Binary/Construct
  • standard-library/src/Relation/Binary/Construct/Union.agda
  • standard-library/src/Relation/Binary/Construct/Subst
  • standard-library/src/Relation/Binary/Construct/Subst/Equality.agda
  • standard-library/src/Relation/Binary/Construct/StrictToNonStrict.agda
  • standard-library/src/Relation/Binary/Construct/On.agda
  • standard-library/src/Relation/Binary/Construct/NonStrictToStrict.agda
  • standard-library/src/Relation/Binary/Construct/Never.agda
  • standard-library/src/Relation/Binary/Construct/NaturalOrder
  • standard-library/src/Relation/Binary/Construct/NaturalOrder/Right.agda
  • standard-library/src/Relation/Binary/Construct/NaturalOrder/Left.agda
  • standard-library/src/Relation/Binary/Construct/Intersection.agda
  • standard-library/src/Relation/Binary/Construct/Interior
  • standard-library/src/Relation/Binary/Construct/Interior/Symmetric.agda
  • standard-library/src/Relation/Binary/Construct/FromRel.agda
  • standard-library/src/Relation/Binary/Construct/FromPred.agda
  • standard-library/src/Relation/Binary/Construct/Flip.agda
  • standard-library/src/Relation/Binary/Construct/Flip
  • standard-library/src/Relation/Binary/Construct/Flip/Ord.agda
  • standard-library/src/Relation/Binary/Construct/Flip/EqAndOrd.agda
  • standard-library/src/Relation/Binary/Construct/Converse.agda
  • standard-library/src/Relation/Binary/Construct/Constant.agda
  • standard-library/src/Relation/Binary/Construct/Constant
  • standard-library/src/Relation/Binary/Construct/Constant/Core.agda
  • standard-library/src/Relation/Binary/Construct/Composition.agda
  • standard-library/src/Relation/Binary/Construct/Closure
  • standard-library/src/Relation/Binary/Construct/Closure/Transitive.agda
  • standard-library/src/Relation/Binary/Construct/Closure/Transitive
  • standard-library/src/Relation/Binary/Construct/Closure/Transitive/WithK.agda
  • standard-library/src/Relation/Binary/Construct/Closure/SymmetricTransitive.agda
  • standard-library/src/Relation/Binary/Construct/Closure/Symmetric.agda
  • standard-library/src/Relation/Binary/Construct/Closure/ReflexiveTransitive.agda
  • standard-library/src/Relation/Binary/Construct/Closure/ReflexiveTransitive
  • standard-library/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties.agda
  • standard-library/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties
  • standard-library/src/Relation/Binary/Construct/Closure/ReflexiveTransitive/Properties/WithK.agda
  • standard-library/src/Relation/Binary/Construct/Closure/Reflexive.agda
  • standard-library/src/Relation/Binary/Construct/Closure/Reflexive
  • standard-library/src/Relation/Binary/Construct/Closure/Reflexive/Properties.agda
  • standard-library/src/Relation/Binary/Construct/Closure/Reflexive/Properties
  • standard-library/src/Relation/Binary/Construct/Closure/Reflexive/Properties/WithK.agda
  • standard-library/src/Relation/Binary/Construct/Closure/Equivalence.agda
  • standard-library/src/Relation/Binary/Construct/Closure/Equivalence
  • standard-library/src/Relation/Binary/Construct/Closure/Equivalence/Properties.agda
  • standard-library/src/Relation/Binary/Construct/Always.agda
  • standard-library/src/Relation/Binary/Construct/Add
  • standard-library/src/Relation/Binary/Construct/Add/Supremum
  • standard-library/src/Relation/Binary/Construct/Add/Supremum/Strict.agda
  • standard-library/src/Relation/Binary/Construct/Add/Supremum/NonStrict.agda
  • standard-library/src/Relation/Binary/Construct/Add/Supremum/Equality.agda
  • standard-library/src/Relation/Binary/Construct/Add/Point
  • standard-library/src/Relation/Binary/Construct/Add/Point/Equality.agda
  • standard-library/src/Relation/Binary/Construct/Add/Infimum
  • standard-library/src/Relation/Binary/Construct/Add/Infimum/Strict.agda
  • standard-library/src/Relation/Binary/Construct/Add/Infimum/NonStrict.agda
  • standard-library/src/Relation/Binary/Construct/Add/Infimum/Equality.agda
  • standard-library/src/Relation/Binary/Construct/Add/Extrema
  • standard-library/src/Relation/Binary/Construct/Add/Extrema/Strict.agda
  • standard-library/src/Relation/Binary/Construct/Add/Extrema/NonStrict.agda
  • standard-library/src/Relation/Binary/Construct/Add/Extrema/Equality.agda
  • standard-library/src/Relation/Binary/Consequences.agda
  • standard-library/src/Relation/Binary/Bundles.agda
  • standard-library/src/Reflection.agda
  • standard-library/src/Reflection
  • standard-library/src/Reflection/TCM.agda
  • standard-library/src/Reflection/TCM
  • standard-library/src/Reflection/TCM/Utilities.agda
  • standard-library/src/Reflection/TCM/Syntax.agda
  • standard-library/src/Reflection/TCM/Instances.agda
  • standard-library/src/Reflection/TCM/Format.agda
  • standard-library/src/Reflection/TCM/Effectful.agda
  • standard-library/src/Reflection/TCM/Categorical.agda
  • standard-library/src/Reflection/External.agda
  • standard-library/src/Reflection/AnnotatedAST.agda
  • standard-library/src/Reflection/AnnotatedAST
  • standard-library/src/Reflection/AnnotatedAST/Free.agda
  • standard-library/src/Reflection/AST.agda
  • standard-library/src/Reflection/AST
  • standard-library/src/Reflection/AST/Universe.agda
  • standard-library/src/Reflection/AST/Traversal.agda
  • standard-library/src/Reflection/AST/Term.agda
  • standard-library/src/Reflection/AST/Show.agda
  • standard-library/src/Reflection/AST/Pattern.agda
  • standard-library/src/Reflection/AST/Name.agda
  • standard-library/src/Reflection/AST/Meta.agda
  • standard-library/src/Reflection/AST/Literal.agda
  • standard-library/src/Reflection/AST/Instances.agda
  • standard-library/src/Reflection/AST/Definition.agda
  • standard-library/src/Reflection/AST/DeBruijn.agda
  • standard-library/src/Reflection/AST/Argument.agda
  • standard-library/src/Reflection/AST/Argument
  • standard-library/src/Reflection/AST/Argument/Visibility.agda
  • standard-library/src/Reflection/AST/Argument/Relevance.agda
  • standard-library/src/Reflection/AST/Argument/Quantity.agda
  • standard-library/src/Reflection/AST/Argument/Modality.agda
  • standard-library/src/Reflection/AST/Argument/Information.agda
  • standard-library/src/Reflection/AST/AlphaEquality.agda
  • standard-library/src/Reflection/AST/Abstraction.agda
  • standard-library/src/Level.agda
  • standard-library/src/Level
  • standard-library/src/Level/Literals.agda
  • standard-library/src/Induction.agda
  • standard-library/src/Induction
  • standard-library/src/Induction/WellFounded.agda
  • standard-library/src/Induction/Lexicographic.agda
  • standard-library/src/Induction/InfiniteDescent.agda
  • standard-library/src/IO.agda
  • standard-library/src/IO
  • standard-library/src/IO/Primitive.agda
  • standard-library/src/IO/Primitive
  • standard-library/src/IO/Primitive/Infinite.agda
  • standard-library/src/IO/Primitive/Handle.agda
  • standard-library/src/IO/Primitive/Finite.agda
  • standard-library/src/IO/Primitive/Core.agda
  • standard-library/src/IO/Instances.agda
  • standard-library/src/IO/Infinite.agda
  • standard-library/src/IO/Handle.agda
  • standard-library/src/IO/Finite.agda
  • standard-library/src/IO/Effectful.agda
  • standard-library/src/IO/Categorical.agda
  • standard-library/src/IO/Base.agda
  • standard-library/src/Function.agda
  • standard-library/src/Function
  • standard-library/src/Function/Surjection.agda
  • standard-library/src/Function/Structures.agda
  • standard-library/src/Function/Structures
  • standard-library/src/Function/Structures/Biased.agda
  • standard-library/src/Function/Strict.agda
  • standard-library/src/Function/Relation
  • standard-library/src/Function/Relation/Binary
  • standard-library/src/Function/Relation/Binary/Setoid
  • standard-library/src/Function/Relation/Binary/Setoid/Equality.agda
  • standard-library/src/Function/Related.agda
  • standard-library/src/Function/Related
  • standard-library/src/Function/Related/TypeIsomorphisms.agda
  • standard-library/src/Function/Related/TypeIsomorphisms
  • standard-library/src/Function/Related/TypeIsomorphisms/Solver.agda
  • standard-library/src/Function/Related/Propositional.agda
  • standard-library/src/Function/Reasoning.agda
  • standard-library/src/Function/Properties.agda
  • standard-library/src/Function/Properties
  • standard-library/src/Function/Properties/Surjection.agda
  • standard-library/src/Function/Properties/RightInverse.agda
  • standard-library/src/Function/Properties/Inverse.agda
  • standard-library/src/Function/Properties/Inverse
  • standard-library/src/Function/Properties/Inverse/HalfAdjointEquivalence.agda
  • standard-library/src/Function/Properties/Injection.agda
  • standard-library/src/Function/Properties/Equivalence.agda
  • standard-library/src/Function/Properties/Bijection.agda
  • standard-library/src/Function/Nary
  • standard-library/src/Function/Nary/NonDependent.agda
  • standard-library/src/Function/Nary/NonDependent
  • standard-library/src/Function/Nary/NonDependent/Base.agda
  • standard-library/src/Function/Metric.agda
  • standard-library/src/Function/Metric
  • standard-library/src/Function/Metric/Structures.agda
  • standard-library/src/Function/Metric/Rational.agda
  • standard-library/src/Function/Metric/Rational
  • standard-library/src/Function/Metric/Rational/Structures.agda
  • standard-library/src/Function/Metric/Rational/Definitions.agda
  • standard-library/src/Function/Metric/Rational/Core.agda
  • standard-library/src/Function/Metric/Rational/Bundles.agda
  • standard-library/src/Function/Metric/Nat.agda
  • standard-library/src/Function/Metric/Nat
  • standard-library/src/Function/Metric/Nat/Structures.agda
  • standard-library/src/Function/Metric/Nat/Definitions.agda
  • standard-library/src/Function/Metric/Nat/Core.agda
  • standard-library/src/Function/Metric/Nat/Bundles.agda
  • standard-library/src/Function/Metric/Definitions.agda
  • standard-library/src/Function/Metric/Core.agda
  • standard-library/src/Function/Metric/Bundles.agda
  • standard-library/src/Function/LeftInverse.agda
  • standard-library/src/Function/Inverse.agda
  • standard-library/src/Function/Injection.agda
  • standard-library/src/Function/Indexed
  • standard-library/src/Function/Indexed/Relation
  • standard-library/src/Function/Indexed/Relation/Binary
  • standard-library/src/Function/Indexed/Relation/Binary/Equality.agda
  • standard-library/src/Function/Indexed/Bundles.agda
  • standard-library/src/Function/Identity
  • standard-library/src/Function/Identity/Effectful.agda
  • standard-library/src/Function/Identity/Categorical.agda
  • standard-library/src/Function/HalfAdjointEquivalence.agda
  • standard-library/src/Function/Equivalence.agda
  • standard-library/src/Function/Equality.agda
  • standard-library/src/Function/Endomorphism
  • standard-library/src/Function/Endomorphism/Setoid.agda
  • standard-library/src/Function/Endomorphism/Propositional.agda
  • standard-library/src/Function/Endo
  • standard-library/src/Function/Endo/Setoid.agda
  • standard-library/src/Function/Endo/Propositional.agda
  • standard-library/src/Function/Dependent
  • standard-library/src/Function/Dependent/Bundles.agda
  • standard-library/src/Function/Definitions.agda
  • standard-library/src/Function/Core.agda
  • standard-library/src/Function/Construct
  • standard-library/src/Function/Construct/Symmetry.agda
  • standard-library/src/Function/Construct/Identity.agda
  • standard-library/src/Function/Construct/Constant.agda
  • standard-library/src/Function/Construct/Composition.agda
  • standard-library/src/Function/Consequences.agda
  • standard-library/src/Function/Consequences
  • standard-library/src/Function/Consequences/Setoid.agda
  • standard-library/src/Function/Consequences/Propositional.agda
  • standard-library/src/Function/Bundles.agda
  • standard-library/src/Function/Bijection.agda
  • standard-library/src/Function/Base.agda
  • standard-library/src/Foreign
  • standard-library/src/Foreign/Haskell.agda
  • standard-library/src/Effect
  • standard-library/src/Effect/Monad.agda
  • standard-library/src/Effect/Monad
  • standard-library/src/Effect/Monad/Writer.agda
  • standard-library/src/Effect/Monad/Writer
  • standard-library/src/Effect/Monad/Writer/Transformer.agda
  • standard-library/src/Effect/Monad/Writer/Transformer
  • standard-library/src/Effect/Monad/Writer/Transformer/Base.agda
  • standard-library/src/Effect/Monad/Writer/Instances.agda
  • standard-library/src/Effect/Monad/Writer/Indexed.agda
  • standard-library/src/Effect/Monad/State.agda
  • standard-library/src/Effect/Monad/State
  • standard-library/src/Effect/Monad/State/Transformer.agda
  • standard-library/src/Effect/Monad/State/Transformer
  • standard-library/src/Effect/Monad/State/Transformer/Base.agda
  • standard-library/src/Effect/Monad/State/Instances.agda
  • standard-library/src/Effect/Monad/State/Indexed.agda
  • standard-library/src/Effect/Monad/Reader.agda
  • standard-library/src/Effect/Monad/Reader
  • standard-library/src/Effect/Monad/Reader/Transformer.agda
  • standard-library/src/Effect/Monad/Reader/Transformer
  • standard-library/src/Effect/Monad/Reader/Transformer/Base.agda
  • standard-library/src/Effect/Monad/Reader/Instances.agda
  • standard-library/src/Effect/Monad/Reader/Indexed.agda
  • standard-library/src/Effect/Monad/Predicate.agda
  • standard-library/src/Effect/Monad/Partiality.agda
  • standard-library/src/Effect/Monad/Partiality
  • standard-library/src/Effect/Monad/Partiality/Instances.agda
  • standard-library/src/Effect/Monad/Partiality/All.agda
  • standard-library/src/Effect/Monad/Indexed.agda
  • standard-library/src/Effect/Monad/Identity.agda
  • standard-library/src/Effect/Monad/Identity
  • standard-library/src/Effect/Monad/Identity/Instances.agda
  • standard-library/src/Effect/Monad/IO.agda
  • standard-library/src/Effect/Monad/IO
  • standard-library/src/Effect/Monad/IO/Instances.agda
  • standard-library/src/Effect/Monad/Error
  • standard-library/src/Effect/Monad/Error/Transformer.agda
  • standard-library/src/Effect/Monad/Continuation.agda
  • standard-library/src/Effect/Functor.agda
  • standard-library/src/Effect/Functor
  • standard-library/src/Effect/Functor/Predicate.agda
  • standard-library/src/Effect/Empty.agda
  • standard-library/src/Effect/Comonad.agda
  • standard-library/src/Effect/Choice.agda
  • standard-library/src/Effect/Applicative.agda
  • standard-library/src/Effect/Applicative
  • standard-library/src/Effect/Applicative/Predicate.agda
  • standard-library/src/Effect/Applicative/Indexed.agda
  • standard-library/src/Debug
  • standard-library/src/Debug/Trace.agda
  • standard-library/src/Data
  • standard-library/src/Data/Wrap.agda
  • standard-library/src/Data/Word8
  • standard-library/src/Data/Word8/Show.agda
  • standard-library/src/Data/Word8/Primitive.agda
  • standard-library/src/Data/Word8/Literals.agda
  • standard-library/src/Data/Word8/Base.agda
  • standard-library/src/Data/Word64.agda
  • standard-library/src/Data/Word64
  • standard-library/src/Data/Word64/Unsafe.agda
  • standard-library/src/Data/Word64/Show.agda
  • standard-library/src/Data/Word64/Properties.agda
  • standard-library/src/Data/Word64/Primitive.agda
  • standard-library/src/Data/Word64/Literals.agda
  • standard-library/src/Data/Word64/Instances.agda
  • standard-library/src/Data/Word64/Base.agda
  • standard-library/src/Data/Word.agda
  • standard-library/src/Data/Word
  • standard-library/src/Data/Word/Properties.agda
  • standard-library/src/Data/Word/Instances.agda
  • standard-library/src/Data/Word/Base.agda
  • standard-library/src/Data/W.agda
  • standard-library/src/Data/W
  • standard-library/src/Data/W/WithK.agda
  • standard-library/src/Data/W/Sized.agda
  • standard-library/src/Data/W/Indexed.agda
  • standard-library/src/Data/Vec.agda
  • standard-library/src/Data/Vec
  • standard-library/src/Data/Vec/Show.agda
  • standard-library/src/Data/Vec/Relation
  • standard-library/src/Data/Vec/Relation/Unary
  • standard-library/src/Data/Vec/Relation/Unary/Unique
  • standard-library/src/Data/Vec/Relation/Unary/Unique/Setoid.agda
  • standard-library/src/Data/Vec/Relation/Unary/Unique/Setoid
  • standard-library/src/Data/Vec/Relation/Unary/Unique/Setoid/Properties.agda
  • standard-library/src/Data/Vec/Relation/Unary/Unique/Propositional.agda
  • standard-library/src/Data/Vec/Relation/Unary/Unique/Propositional
  • standard-library/src/Data/Vec/Relation/Unary/Unique/Propositional/Properties.agda
  • standard-library/src/Data/Vec/Relation/Unary/Linked.agda
  • standard-library/src/Data/Vec/Relation/Unary/Linked
  • standard-library/src/Data/Vec/Relation/Unary/Linked/Properties.agda
  • standard-library/src/Data/Vec/Relation/Unary/Any.agda
  • standard-library/src/Data/Vec/Relation/Unary/Any
  • standard-library/src/Data/Vec/Relation/Unary/Any/Properties.agda
  • standard-library/src/Data/Vec/Relation/Unary/AllPairs.agda
  • standard-library/src/Data/Vec/Relation/Unary/AllPairs
  • standard-library/src/Data/Vec/Relation/Unary/AllPairs/Properties.agda
  • standard-library/src/Data/Vec/Relation/Unary/AllPairs/Core.agda
  • standard-library/src/Data/Vec/Relation/Unary/All.agda
  • standard-library/src/Data/Vec/Relation/Unary/All
  • standard-library/src/Data/Vec/Relation/Unary/All/Properties.agda
  • standard-library/src/Data/Vec/Relation/Binary
  • standard-library/src/Data/Vec/Relation/Binary/Pointwise
  • standard-library/src/Data/Vec/Relation/Binary/Pointwise/Inductive.agda
  • standard-library/src/Data/Vec/Relation/Binary/Pointwise/Extensional.agda
  • standard-library/src/Data/Vec/Relation/Binary/Lex
  • standard-library/src/Data/Vec/Relation/Binary/Lex/Strict.agda
  • standard-library/src/Data/Vec/Relation/Binary/Lex/NonStrict.agda
  • standard-library/src/Data/Vec/Relation/Binary/Lex/Core.agda
  • standard-library/src/Data/Vec/Relation/Binary/Equality
  • standard-library/src/Data/Vec/Relation/Binary/Equality/Setoid.agda
  • standard-library/src/Data/Vec/Relation/Binary/Equality/Propositional.agda
  • standard-library/src/Data/Vec/Relation/Binary/Equality/Propositional
  • standard-library/src/Data/Vec/Relation/Binary/Equality/Propositional/WithK.agda
  • standard-library/src/Data/Vec/Relation/Binary/Equality/DecSetoid.agda
  • standard-library/src/Data/Vec/Relation/Binary/Equality/DecPropositional.agda
  • standard-library/src/Data/Vec/Relation/Binary/Equality/Cast.agda
  • standard-library/src/Data/Vec/Reflection.agda
  • standard-library/src/Data/Vec/Recursive.agda
  • standard-library/src/Data/Vec/Recursive
  • standard-library/src/Data/Vec/Recursive/Properties.agda
  • standard-library/src/Data/Vec/Recursive/Effectful.agda
  • standard-library/src/Data/Vec/Recursive/Categorical.agda
  • standard-library/src/Data/Vec/Properties.agda
  • standard-library/src/Data/Vec/Properties
  • standard-library/src/Data/Vec/Properties/WithK.agda
  • standard-library/src/Data/Vec/N-ary.agda
  • standard-library/src/Data/Vec/Membership
  • standard-library/src/Data/Vec/Membership/Setoid.agda
  • standard-library/src/Data/Vec/Membership/Propositional.agda
  • standard-library/src/Data/Vec/Membership/Propositional
  • standard-library/src/Data/Vec/Membership/Propositional/Properties.agda
  • standard-library/src/Data/Vec/Membership/DecSetoid.agda
  • standard-library/src/Data/Vec/Membership/DecPropositional.agda
  • standard-library/src/Data/Vec/Instances.agda
  • standard-library/src/Data/Vec/Functional.agda
  • standard-library/src/Data/Vec/Functional
  • standard-library/src/Data/Vec/Functional/Relation
  • standard-library/src/Data/Vec/Functional/Relation/Unary
  • standard-library/src/Data/Vec/Functional/Relation/Unary/Any.agda
  • standard-library/src/Data/Vec/Functional/Relation/Unary/All.agda
  • standard-library/src/Data/Vec/Functional/Relation/Unary/All
  • standard-library/src/Data/Vec/Functional/Relation/Unary/All/Properties.agda
  • standard-library/src/Data/Vec/Functional/Relation/Binary
  • standard-library/src/Data/Vec/Functional/Relation/Binary/Pointwise.agda
  • standard-library/src/Data/Vec/Functional/Relation/Binary/Pointwise
  • standard-library/src/Data/Vec/Functional/Relation/Binary/Pointwise/Properties.agda
  • standard-library/src/Data/Vec/Functional/Relation/Binary/Permutation.agda
  • standard-library/src/Data/Vec/Functional/Relation/Binary/Permutation
  • standard-library/src/Data/Vec/Functional/Relation/Binary/Permutation/Properties.agda
  • standard-library/src/Data/Vec/Functional/Relation/Binary/Equality
  • standard-library/src/Data/Vec/Functional/Relation/Binary/Equality/Setoid.agda
  • standard-library/src/Data/Vec/Functional/Properties.agda
  • standard-library/src/Data/Vec/Effectful.agda
  • standard-library/src/Data/Vec/Effectful
  • standard-library/src/Data/Vec/Effectful/Transformer.agda
  • standard-library/src/Data/Vec/Categorical.agda
  • standard-library/src/Data/Vec/Categorical
  • standard-library/src/Data/Vec/Categorical/Transformer.agda
  • standard-library/src/Data/Vec/Bounded.agda
  • standard-library/src/Data/Vec/Bounded
  • standard-library/src/Data/Vec/Bounded/Show.agda
  • standard-library/src/Data/Vec/Bounded/Base.agda
  • standard-library/src/Data/Vec/Base.agda
  • standard-library/src/Data/Universe.agda
  • standard-library/src/Data/Universe
  • standard-library/src/Data/Universe/Indexed.agda
  • standard-library/src/Data/Unit.agda
  • standard-library/src/Data/Unit
  • standard-library/src/Data/Unit/Properties.agda
  • standard-library/src/Data/Unit/Polymorphic.agda
  • standard-library/src/Data/Unit/Polymorphic
  • standard-library/src/Data/Unit/Polymorphic/Properties.agda
  • standard-library/src/Data/Unit/Polymorphic/Instances.agda
  • standard-library/src/Data/Unit/Polymorphic/Base.agda
  • standard-library/src/Data/Unit/NonEta.agda
  • standard-library/src/Data/Unit/Instances.agda
  • standard-library/src/Data/Unit/Base.agda
  • standard-library/src/Data/Trie.agda
  • standard-library/src/Data/Trie
  • standard-library/src/Data/Trie/NonEmpty.agda
  • standard-library/src/Data/Tree
  • standard-library/src/Data/Tree/Rose.agda
  • standard-library/src/Data/Tree/Rose
  • standard-library/src/Data/Tree/Rose/Show.agda
  • standard-library/src/Data/Tree/Rose/Properties.agda
  • standard-library/src/Data/Tree/Binary.agda
  • standard-library/src/Data/Tree/Binary
  • standard-library/src/Data/Tree/Binary/Zipper.agda
  • standard-library/src/Data/Tree/Binary/Zipper
  • standard-library/src/Data/Tree/Binary/Zipper/Properties.agda
  • standard-library/src/Data/Tree/Binary/Show.agda
  • standard-library/src/Data/Tree/Binary/Relation
  • standard-library/src/Data/Tree/Binary/Relation/Unary
  • standard-library/src/Data/Tree/Binary/Relation/Unary/All.agda
  • standard-library/src/Data/Tree/Binary/Relation/Unary/All
  • standard-library/src/Data/Tree/Binary/Relation/Unary/All/Properties.agda
  • standard-library/src/Data/Tree/Binary/Properties.agda
  • standard-library/src/Data/Tree/AVL.agda
  • standard-library/src/Data/Tree/AVL
  • standard-library/src/Data/Tree/AVL/Value.agda
  • standard-library/src/Data/Tree/AVL/Sets.agda
  • standard-library/src/Data/Tree/AVL/Sets
  • standard-library/src/Data/Tree/AVL/Sets/Membership.agda
  • standard-library/src/Data/Tree/AVL/Sets/Membership
  • standard-library/src/Data/Tree/AVL/Sets/Membership/Properties.agda
  • standard-library/src/Data/Tree/AVL/Relation
  • standard-library/src/Data/Tree/AVL/Relation/Unary
  • standard-library/src/Data/Tree/AVL/Relation/Unary/Any.agda
  • standard-library/src/Data/Tree/AVL/NonEmpty.agda
  • standard-library/src/Data/Tree/AVL/NonEmpty
  • standard-library/src/Data/Tree/AVL/NonEmpty/Propositional.agda
  • standard-library/src/Data/Tree/AVL/Map.agda
  • standard-library/src/Data/Tree/AVL/Map
  • standard-library/src/Data/Tree/AVL/Map/Relation
  • standard-library/src/Data/Tree/AVL/Map/Relation/Unary
  • standard-library/src/Data/Tree/AVL/Map/Relation/Unary/Any.agda
  • standard-library/src/Data/Tree/AVL/Map/Membership
  • standard-library/src/Data/Tree/AVL/Map/Membership/Propositional.agda
  • standard-library/src/Data/Tree/AVL/Map/Membership/Propositional
  • standard-library/src/Data/Tree/AVL/Map/Membership/Propositional/Properties.agda
  • standard-library/src/Data/Tree/AVL/Key.agda
  • standard-library/src/Data/Tree/AVL/IndexedMap.agda
  • standard-library/src/Data/Tree/AVL/Indexed.agda
  • standard-library/src/Data/Tree/AVL/Indexed
  • standard-library/src/Data/Tree/AVL/Indexed/WithK.agda
  • standard-library/src/Data/Tree/AVL/Indexed/Relation
  • standard-library/src/Data/Tree/AVL/Indexed/Relation/Unary
  • standard-library/src/Data/Tree/AVL/Indexed/Relation/Unary/Any.agda
  • standard-library/src/Data/Tree/AVL/Indexed/Relation/Unary/Any
  • standard-library/src/Data/Tree/AVL/Indexed/Relation/Unary/Any/Properties.agda
  • standard-library/src/Data/Tree/AVL/Indexed/Relation/Unary/All.agda
  • standard-library/src/Data/Tree/AVL/Height.agda
  • standard-library/src/Data/These.agda
  • standard-library/src/Data/These
  • standard-library/src/Data/These/Properties.agda
  • standard-library/src/Data/These/Instances.agda
  • standard-library/src/Data/These/Effectful
  • standard-library/src/Data/These/Effectful/Right.agda
  • standard-library/src/Data/These/Effectful/Right
  • standard-library/src/Data/These/Effectful/Right/Base.agda
  • standard-library/src/Data/These/Effectful/Left.agda
  • standard-library/src/Data/These/Effectful/Left
  • standard-library/src/Data/These/Effectful/Left/Base.agda
  • standard-library/src/Data/These/Categorical
  • standard-library/src/Data/These/Categorical/Right.agda
  • standard-library/src/Data/These/Categorical/Right
  • standard-library/src/Data/These/Categorical/Right/Base.agda
  • standard-library/src/Data/These/Categorical/Left.agda
  • standard-library/src/Data/These/Categorical/Left
  • standard-library/src/Data/These/Categorical/Left/Base.agda
  • standard-library/src/Data/These/Base.agda
  • standard-library/src/Data/Sum.agda
  • standard-library/src/Data/Sum
  • standard-library/src/Data/Sum/Relation
  • standard-library/src/Data/Sum/Relation/Unary
  • standard-library/src/Data/Sum/Relation/Unary/All.agda
  • standard-library/src/Data/Sum/Relation/Binary
  • standard-library/src/Data/Sum/Relation/Binary/Pointwise.agda
  • standard-library/src/Data/Sum/Relation/Binary/LeftOrder.agda
  • standard-library/src/Data/Sum/Properties.agda
  • standard-library/src/Data/Sum/Instances.agda
  • standard-library/src/Data/Sum/Function
  • standard-library/src/Data/Sum/Function/Setoid.agda
  • standard-library/src/Data/Sum/Function/Propositional.agda
  • standard-library/src/Data/Sum/Effectful
  • standard-library/src/Data/Sum/Effectful/Right.agda
  • standard-library/src/Data/Sum/Effectful/Right
  • standard-library/src/Data/Sum/Effectful/Right/Transformer.agda
  • standard-library/src/Data/Sum/Effectful/Left.agda
  • standard-library/src/Data/Sum/Effectful/Left
  • standard-library/src/Data/Sum/Effectful/Left/Transformer.agda
  • standard-library/src/Data/Sum/Effectful/Examples.agda
  • standard-library/src/Data/Sum/Categorical
  • standard-library/src/Data/Sum/Categorical/Right.agda
  • standard-library/src/Data/Sum/Categorical/Right
  • standard-library/src/Data/Sum/Categorical/Right/Transformer.agda
  • standard-library/src/Data/Sum/Categorical/Left.agda
  • standard-library/src/Data/Sum/Categorical/Left
  • standard-library/src/Data/Sum/Categorical/Left/Transformer.agda
  • standard-library/src/Data/Sum/Categorical/Examples.agda
  • standard-library/src/Data/Sum/Base.agda
  • standard-library/src/Data/Sum/Algebra.agda
  • standard-library/src/Data/String.agda
  • standard-library/src/Data/String
  • standard-library/src/Data/String/Unsafe.agda
  • standard-library/src/Data/String/Properties.agda
  • standard-library/src/Data/String/Literals.agda
  • standard-library/src/Data/String/Instances.agda
  • standard-library/src/Data/String/Base.agda
  • standard-library/src/Data/Star
  • standard-library/src/Data/Star/Vec.agda
  • standard-library/src/Data/Star/Pointer.agda
  • standard-library/src/Data/Star/Nat.agda
  • standard-library/src/Data/Star/List.agda
  • standard-library/src/Data/Star/Fin.agda
  • standard-library/src/Data/Star/Environment.agda
  • standard-library/src/Data/Star/Decoration.agda
  • standard-library/src/Data/Star/BoundedVec.agda
  • standard-library/src/Data/Sign.agda
  • standard-library/src/Data/Sign
  • standard-library/src/Data/Sign/Properties.agda
  • standard-library/src/Data/Sign/Instances.agda
  • standard-library/src/Data/Sign/Base.agda
  • standard-library/src/Data/Refinement.agda
  • standard-library/src/Data/Refinement
  • standard-library/src/Data/Refinement/Relation
  • standard-library/src/Data/Refinement/Relation/Unary
  • standard-library/src/Data/Refinement/Relation/Unary/All.agda
  • standard-library/src/Data/Record.agda
  • standard-library/src/Data/Rational.agda
  • standard-library/src/Data/Rational
  • standard-library/src/Data/Rational/Unnormalised.agda
  • standard-library/src/Data/Rational/Unnormalised
  • standard-library/src/Data/Rational/Unnormalised/Solver.agda
  • standard-library/src/Data/Rational/Unnormalised/Show.agda
  • standard-library/src/Data/Rational/Unnormalised/Properties.agda
  • standard-library/src/Data/Rational/Unnormalised/Base.agda
  • standard-library/src/Data/Rational/Solver.agda
  • standard-library/src/Data/Rational/Show.agda
  • standard-library/src/Data/Rational/Properties.agda
  • standard-library/src/Data/Rational/Literals.agda
  • standard-library/src/Data/Rational/Instances.agda
  • standard-library/src/Data/Rational/Base.agda
  • standard-library/src/Data/Product.agda
  • standard-library/src/Data/Product
  • standard-library/src/Data/Product/Relation
  • standard-library/src/Data/Product/Relation/Unary
  • standard-library/src/Data/Product/Relation/Unary/All.agda
  • standard-library/src/Data/Product/Relation/Binary
  • standard-library/src/Data/Product/Relation/Binary/Pointwise
  • standard-library/src/Data/Product/Relation/Binary/Pointwise/NonDependent.agda
  • standard-library/src/Data/Product/Relation/Binary/Pointwise/Dependent.agda
  • standard-library/src/Data/Product/Relation/Binary/Pointwise/Dependent
  • standard-library/src/Data/Product/Relation/Binary/Pointwise/Dependent/WithK.agda
  • standard-library/src/Data/Product/Relation/Binary/Lex
  • standard-library/src/Data/Product/Relation/Binary/Lex/Strict.agda
  • standard-library/src/Data/Product/Relation/Binary/Lex/NonStrict.agda
  • standard-library/src/Data/Product/Properties.agda
  • standard-library/src/Data/Product/Properties
  • standard-library/src/Data/Product/Properties/WithK.agda
  • standard-library/src/Data/Product/Properties/Dependent.agda
  • standard-library/src/Data/Product/Nary
  • standard-library/src/Data/Product/Nary/NonDependent.agda
  • standard-library/src/Data/Product/Instances.agda
  • standard-library/src/Data/Product/Function
  • standard-library/src/Data/Product/Function/NonDependent
  • standard-library/src/Data/Product/Function/NonDependent/Setoid.agda
  • standard-library/src/Data/Product/Function/NonDependent/Propositional.agda
  • standard-library/src/Data/Product/Function/Dependent
  • standard-library/src/Data/Product/Function/Dependent/Setoid.agda
  • standard-library/src/Data/Product/Function/Dependent/Setoid
  • standard-library/src/Data/Product/Function/Dependent/Setoid/WithK.agda
  • standard-library/src/Data/Product/Function/Dependent/Propositional.agda
  • standard-library/src/Data/Product/Function/Dependent/Propositional
  • standard-library/src/Data/Product/Function/Dependent/Propositional/WithK.agda
  • standard-library/src/Data/Product/Effectful
  • standard-library/src/Data/Product/Effectful/Right.agda
  • standard-library/src/Data/Product/Effectful/Right
  • standard-library/src/Data/Product/Effectful/Right/Base.agda
  • standard-library/src/Data/Product/Effectful/Left.agda
  • standard-library/src/Data/Product/Effectful/Left
  • standard-library/src/Data/Product/Effectful/Left/Base.agda
  • standard-library/src/Data/Product/Effectful/Examples.agda
  • standard-library/src/Data/Product/Categorical
  • standard-library/src/Data/Product/Categorical/Right.agda
  • standard-library/src/Data/Product/Categorical/Right
  • standard-library/src/Data/Product/Categorical/Right/Base.agda
  • standard-library/src/Data/Product/Categorical/Left.agda
  • standard-library/src/Data/Product/Categorical/Left
  • standard-library/src/Data/Product/Categorical/Left/Base.agda
  • standard-library/src/Data/Product/Categorical/Examples.agda
  • standard-library/src/Data/Product/Base.agda
  • standard-library/src/Data/Product/Algebra.agda
  • standard-library/src/Data/Parity.agda
  • standard-library/src/Data/Parity
  • standard-library/src/Data/Parity/Properties.agda
  • standard-library/src/Data/Parity/Instances.agda
  • standard-library/src/Data/Parity/Base.agda
  • standard-library/src/Data/Nat.agda
  • standard-library/src/Data/Nat
  • standard-library/src/Data/Nat/WithK.agda
  • standard-library/src/Data/Nat/Tactic
  • standard-library/src/Data/Nat/Tactic/RingSolver.agda
  • standard-library/src/Data/Nat/Solver.agda
  • standard-library/src/Data/Nat/Show.agda
  • standard-library/src/Data/Nat/Show
  • standard-library/src/Data/Nat/Show/Properties.agda
  • standard-library/src/Data/Nat/Reflection.agda
  • standard-library/src/Data/Nat/PseudoRandom
  • standard-library/src/Data/Nat/PseudoRandom/LCG.agda
  • standard-library/src/Data/Nat/PseudoRandom/LCG
  • standard-library/src/Data/Nat/PseudoRandom/LCG/Unsafe.agda
  • standard-library/src/Data/Nat/Properties.agda
  • standard-library/src/Data/Nat/Properties
  • standard-library/src/Data/Nat/Properties/Core.agda
  • standard-library/src/Data/Nat/Primality.agda
  • standard-library/src/Data/Nat/Primality
  • standard-library/src/Data/Nat/Primality/Factorisation.agda
  • standard-library/src/Data/Nat/Logarithm.agda
  • standard-library/src/Data/Nat/Logarithm
  • standard-library/src/Data/Nat/Logarithm/Core.agda
  • standard-library/src/Data/Nat/Literals.agda
  • standard-library/src/Data/Nat/LCM.agda
  • standard-library/src/Data/Nat/Instances.agda
  • standard-library/src/Data/Nat/InfinitelyOften.agda
  • standard-library/src/Data/Nat/Induction.agda
  • standard-library/src/Data/Nat/GeneralisedArithmetic.agda
  • standard-library/src/Data/Nat/GCD.agda
  • standard-library/src/Data/Nat/GCD
  • standard-library/src/Data/Nat/GCD/Lemmas.agda
  • standard-library/src/Data/Nat/Divisibility.agda
  • standard-library/src/Data/Nat/Divisibility
  • standard-library/src/Data/Nat/Divisibility/Core.agda
  • standard-library/src/Data/Nat/DivMod.agda
  • standard-library/src/Data/Nat/DivMod
  • standard-library/src/Data/Nat/DivMod/WithK.agda
  • standard-library/src/Data/Nat/DivMod/Core.agda
  • standard-library/src/Data/Nat/Coprimality.agda
  • standard-library/src/Data/Nat/Combinatorics.agda
  • standard-library/src/Data/Nat/Combinatorics
  • standard-library/src/Data/Nat/Combinatorics/Specification.agda
  • standard-library/src/Data/Nat/Combinatorics/Base.agda
  • standard-library/src/Data/Nat/Binary.agda
  • standard-library/src/Data/Nat/Binary
  • standard-library/src/Data/Nat/Binary/Subtraction.agda
  • standard-library/src/Data/Nat/Binary/Properties.agda
  • standard-library/src/Data/Nat/Binary/Instances.agda
  • standard-library/src/Data/Nat/Binary/Induction.agda
  • standard-library/src/Data/Nat/Binary/Base.agda
  • standard-library/src/Data/Nat/Base.agda
  • standard-library/src/Data/Maybe.agda
  • standard-library/src/Data/Maybe
  • standard-library/src/Data/Maybe/Relation
  • standard-library/src/Data/Maybe/Relation/Unary
  • standard-library/src/Data/Maybe/Relation/Unary/Any.agda
  • standard-library/src/Data/Maybe/Relation/Unary/All.agda
  • standard-library/src/Data/Maybe/Relation/Unary/All
  • standard-library/src/Data/Maybe/Relation/Unary/All/Properties.agda
  • standard-library/src/Data/Maybe/Relation/Binary
  • standard-library/src/Data/Maybe/Relation/Binary/Pointwise.agda
  • standard-library/src/Data/Maybe/Relation/Binary/Connected.agda
  • standard-library/src/Data/Maybe/Properties.agda
  • standard-library/src/Data/Maybe/Instances.agda
  • standard-library/src/Data/Maybe/Effectful.agda
  • standard-library/src/Data/Maybe/Effectful
  • standard-library/src/Data/Maybe/Effectful/Transformer.agda
  • standard-library/src/Data/Maybe/Categorical.agda
  • standard-library/src/Data/Maybe/Categorical
  • standard-library/src/Data/Maybe/Categorical/Transformer.agda
  • standard-library/src/Data/Maybe/Base.agda
  • standard-library/src/Data/List.agda
  • standard-library/src/Data/List
  • standard-library/src/Data/List/Zipper.agda
  • standard-library/src/Data/List/Zipper
  • standard-library/src/Data/List/Zipper/Properties.agda
  • standard-library/src/Data/List/Sort.agda
  • standard-library/src/Data/List/Sort
  • standard-library/src/Data/List/Sort/MergeSort.agda
  • standard-library/src/Data/List/Sort/Base.agda
  • standard-library/src/Data/List/Solver.agda
  • standard-library/src/Data/List/Show.agda
  • standard-library/src/Data/List/Scans
  • standard-library/src/Data/List/Scans/Properties.agda
  • standard-library/src/Data/List/Scans/Base.agda
  • standard-library/src/Data/List/Reverse.agda
  • standard-library/src/Data/List/Relation
  • standard-library/src/Data/List/Relation/Unary
  • standard-library/src/Data/List/Relation/Unary/Unique
  • standard-library/src/Data/List/Relation/Unary/Unique/Setoid.agda
  • standard-library/src/Data/List/Relation/Unary/Unique/Setoid
  • standard-library/src/Data/List/Relation/Unary/Unique/Setoid/Properties.agda
  • standard-library/src/Data/List/Relation/Unary/Unique/Propositional.agda
  • standard-library/src/Data/List/Relation/Unary/Unique/Propositional
  • standard-library/src/Data/List/Relation/Unary/Unique/Propositional/Properties.agda
  • standard-library/src/Data/List/Relation/Unary/Unique/DecSetoid.agda
  • standard-library/src/Data/List/Relation/Unary/Unique/DecSetoid
  • standard-library/src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda
  • standard-library/src/Data/List/Relation/Unary/Unique/DecPropositional.agda
  • standard-library/src/Data/List/Relation/Unary/Unique/DecPropositional
  • standard-library/src/Data/List/Relation/Unary/Unique/DecPropositional/Properties.agda
  • standard-library/src/Data/List/Relation/Unary/Sufficient.agda
  • standard-library/src/Data/List/Relation/Unary/Sorted
  • standard-library/src/Data/List/Relation/Unary/Sorted/TotalOrder.agda
  • standard-library/src/Data/List/Relation/Unary/Sorted/TotalOrder
  • standard-library/src/Data/List/Relation/Unary/Sorted/TotalOrder/Properties.agda
  • standard-library/src/Data/List/Relation/Unary/Linked.agda
  • standard-library/src/Data/List/Relation/Unary/Linked
  • standard-library/src/Data/List/Relation/Unary/Linked/Properties.agda
  • standard-library/src/Data/List/Relation/Unary/Grouped.agda
  • standard-library/src/Data/List/Relation/Unary/Grouped
  • standard-library/src/Data/List/Relation/Unary/Grouped/Properties.agda
  • standard-library/src/Data/List/Relation/Unary/First.agda
  • standard-library/src/Data/List/Relation/Unary/First
  • standard-library/src/Data/List/Relation/Unary/First/Properties.agda
  • standard-library/src/Data/List/Relation/Unary/Enumerates
  • standard-library/src/Data/List/Relation/Unary/Enumerates/Setoid.agda
  • standard-library/src/Data/List/Relation/Unary/Enumerates/Setoid
  • standard-library/src/Data/List/Relation/Unary/Enumerates/Setoid/Properties.agda
  • standard-library/src/Data/List/Relation/Unary/Any.agda
  • standard-library/src/Data/List/Relation/Unary/Any
  • standard-library/src/Data/List/Relation/Unary/Any/Properties.agda
  • standard-library/src/Data/List/Relation/Unary/AllPairs.agda
  • standard-library/src/Data/List/Relation/Unary/AllPairs
  • standard-library/src/Data/List/Relation/Unary/AllPairs/Properties.agda
  • standard-library/src/Data/List/Relation/Unary/AllPairs/Core.agda
  • standard-library/src/Data/List/Relation/Unary/All.agda
  • standard-library/src/Data/List/Relation/Unary/All
  • standard-library/src/Data/List/Relation/Unary/All/Properties.agda
  • standard-library/src/Data/List/Relation/Ternary
  • standard-library/src/Data/List/Relation/Ternary/Interleaving.agda
  • standard-library/src/Data/List/Relation/Ternary/Interleaving
  • standard-library/src/Data/List/Relation/Ternary/Interleaving/Setoid.agda
  • standard-library/src/Data/List/Relation/Ternary/Interleaving/Setoid
  • standard-library/src/Data/List/Relation/Ternary/Interleaving/Setoid/Properties.agda
  • standard-library/src/Data/List/Relation/Ternary/Interleaving/Propositional.agda
  • standard-library/src/Data/List/Relation/Ternary/Interleaving/Propositional
  • standard-library/src/Data/List/Relation/Ternary/Interleaving/Propositional/Properties.agda
  • standard-library/src/Data/List/Relation/Ternary/Interleaving/Properties.agda
  • standard-library/src/Data/List/Relation/Ternary/Appending.agda
  • standard-library/src/Data/List/Relation/Ternary/Appending
  • standard-library/src/Data/List/Relation/Ternary/Appending/Setoid.agda
  • standard-library/src/Data/List/Relation/Ternary/Appending/Setoid
  • standard-library/src/Data/List/Relation/Ternary/Appending/Setoid/Properties.agda
  • standard-library/src/Data/List/Relation/Ternary/Appending/Propositional.agda
  • standard-library/src/Data/List/Relation/Ternary/Appending/Propositional
  • standard-library/src/Data/List/Relation/Ternary/Appending/Propositional/Properties.agda
  • standard-library/src/Data/List/Relation/Ternary/Appending/Properties.agda
  • standard-library/src/Data/List/Relation/Binary
  • standard-library/src/Data/List/Relation/Binary/Suffix
  • standard-library/src/Data/List/Relation/Binary/Suffix/Homogeneous
  • standard-library/src/Data/List/Relation/Binary/Suffix/Homogeneous/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Suffix/Heterogeneous.agda
  • standard-library/src/Data/List/Relation/Binary/Suffix/Heterogeneous
  • standard-library/src/Data/List/Relation/Binary/Suffix/Heterogeneous/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Subset
  • standard-library/src/Data/List/Relation/Binary/Subset/Setoid.agda
  • standard-library/src/Data/List/Relation/Binary/Subset/Setoid
  • standard-library/src/Data/List/Relation/Binary/Subset/Setoid/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Subset/Propositional.agda
  • standard-library/src/Data/List/Relation/Binary/Subset/Propositional
  • standard-library/src/Data/List/Relation/Binary/Subset/Propositional/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Subset/DecSetoid.agda
  • standard-library/src/Data/List/Relation/Binary/Subset/DecPropositional.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist
  • standard-library/src/Data/List/Relation/Binary/Sublist/Setoid.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/Setoid
  • standard-library/src/Data/List/Relation/Binary/Sublist/Setoid/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/Propositional.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/Propositional
  • standard-library/src/Data/List/Relation/Binary/Sublist/Propositional/Slice.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/Propositional/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/Propositional/Example
  • standard-library/src/Data/List/Relation/Binary/Sublist/Propositional/Example/UniqueBoundVariables.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/Propositional/Disjoint.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/Heterogeneous.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/Heterogeneous
  • standard-library/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Solver.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/Heterogeneous/Core.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/DecSetoid.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/DecSetoid
  • standard-library/src/Data/List/Relation/Binary/Sublist/DecSetoid/Solver.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/DecPropositional.agda
  • standard-library/src/Data/List/Relation/Binary/Sublist/DecPropositional
  • standard-library/src/Data/List/Relation/Binary/Sublist/DecPropositional/Solver.agda
  • standard-library/src/Data/List/Relation/Binary/Prefix
  • standard-library/src/Data/List/Relation/Binary/Prefix/Homogeneous
  • standard-library/src/Data/List/Relation/Binary/Prefix/Homogeneous/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Prefix/Heterogeneous.agda
  • standard-library/src/Data/List/Relation/Binary/Prefix/Heterogeneous
  • standard-library/src/Data/List/Relation/Binary/Prefix/Heterogeneous/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Pointwise.agda
  • standard-library/src/Data/List/Relation/Binary/Pointwise
  • standard-library/src/Data/List/Relation/Binary/Pointwise/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Pointwise/Base.agda
  • standard-library/src/Data/List/Relation/Binary/Permutation
  • standard-library/src/Data/List/Relation/Binary/Permutation/Setoid.agda
  • standard-library/src/Data/List/Relation/Binary/Permutation/Setoid
  • standard-library/src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Permutation/Setoid/Properties
  • standard-library/src/Data/List/Relation/Binary/Permutation/Setoid/Properties/Maybe.agda
  • standard-library/src/Data/List/Relation/Binary/Permutation/Propositional.agda
  • standard-library/src/Data/List/Relation/Binary/Permutation/Propositional
  • standard-library/src/Data/List/Relation/Binary/Permutation/Propositional/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Permutation/Homogeneous.agda
  • standard-library/src/Data/List/Relation/Binary/Lex.agda
  • standard-library/src/Data/List/Relation/Binary/Lex
  • standard-library/src/Data/List/Relation/Binary/Lex/Strict.agda
  • standard-library/src/Data/List/Relation/Binary/Lex/NonStrict.agda
  • standard-library/src/Data/List/Relation/Binary/Lex/Core.agda
  • standard-library/src/Data/List/Relation/Binary/Infix
  • standard-library/src/Data/List/Relation/Binary/Infix/Homogeneous
  • standard-library/src/Data/List/Relation/Binary/Infix/Homogeneous/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Infix/Heterogeneous.agda
  • standard-library/src/Data/List/Relation/Binary/Infix/Heterogeneous
  • standard-library/src/Data/List/Relation/Binary/Infix/Heterogeneous/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Equality
  • standard-library/src/Data/List/Relation/Binary/Equality/Setoid.agda
  • standard-library/src/Data/List/Relation/Binary/Equality/Setoid
  • standard-library/src/Data/List/Relation/Binary/Equality/Setoid/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Equality/Propositional.agda
  • standard-library/src/Data/List/Relation/Binary/Equality/DecSetoid.agda
  • standard-library/src/Data/List/Relation/Binary/Equality/DecPropositional.agda
  • standard-library/src/Data/List/Relation/Binary/Disjoint
  • standard-library/src/Data/List/Relation/Binary/Disjoint/Setoid.agda
  • standard-library/src/Data/List/Relation/Binary/Disjoint/Setoid
  • standard-library/src/Data/List/Relation/Binary/Disjoint/Setoid/Properties.agda
  • standard-library/src/Data/List/Relation/Binary/Disjoint/Propositional.agda
  • standard-library/src/Data/List/Relation/Binary/Disjoint/DecSetoid.agda
  • standard-library/src/Data/List/Relation/Binary/Disjoint/DecPropositional.agda
  • standard-library/src/Data/List/Relation/Binary/BagAndSetEquality.agda
  • standard-library/src/Data/List/Reflection.agda
  • standard-library/src/Data/List/Properties.agda
  • standard-library/src/Data/List/NonEmpty.agda
  • standard-library/src/Data/List/NonEmpty
  • standard-library/src/Data/List/NonEmpty/Relation
  • standard-library/src/Data/List/NonEmpty/Relation/Unary
  • standard-library/src/Data/List/NonEmpty/Relation/Unary/All.agda
  • standard-library/src/Data/List/NonEmpty/Properties.agda
  • standard-library/src/Data/List/NonEmpty/Instances.agda
  • standard-library/src/Data/List/NonEmpty/Effectful.agda
  • standard-library/src/Data/List/NonEmpty/Effectful
  • standard-library/src/Data/List/NonEmpty/Effectful/Transformer.agda
  • standard-library/src/Data/List/NonEmpty/Categorical.agda
  • standard-library/src/Data/List/NonEmpty/Categorical
  • standard-library/src/Data/List/NonEmpty/Categorical/Transformer.agda
  • standard-library/src/Data/List/NonEmpty/Base.agda
  • standard-library/src/Data/List/Nary
  • standard-library/src/Data/List/Nary/NonDependent.agda
  • standard-library/src/Data/List/Membership
  • standard-library/src/Data/List/Membership/Setoid.agda
  • standard-library/src/Data/List/Membership/Setoid
  • standard-library/src/Data/List/Membership/Setoid/Properties.agda
  • standard-library/src/Data/List/Membership/Propositional.agda
  • standard-library/src/Data/List/Membership/Propositional
  • standard-library/src/Data/List/Membership/Propositional/Properties.agda
  • standard-library/src/Data/List/Membership/Propositional/Properties
  • standard-library/src/Data/List/Membership/Propositional/Properties/WithK.agda
  • standard-library/src/Data/List/Membership/Propositional/Properties/Core.agda
  • standard-library/src/Data/List/Membership/DecSetoid.agda
  • standard-library/src/Data/List/Membership/DecPropositional.agda
  • standard-library/src/Data/List/Literals.agda
  • standard-library/src/Data/List/Kleene.agda
  • standard-library/src/Data/List/Kleene
  • standard-library/src/Data/List/Kleene/Base.agda
  • standard-library/src/Data/List/Kleene/AsList.agda
  • standard-library/src/Data/List/Instances.agda
  • standard-library/src/Data/List/Fresh.agda
  • standard-library/src/Data/List/Fresh
  • standard-library/src/Data/List/Fresh/Relation
  • standard-library/src/Data/List/Fresh/Relation/Unary
  • standard-library/src/Data/List/Fresh/Relation/Unary/Any.agda
  • standard-library/src/Data/List/Fresh/Relation/Unary/Any
  • standard-library/src/Data/List/Fresh/Relation/Unary/Any/Properties.agda
  • standard-library/src/Data/List/Fresh/Relation/Unary/All.agda
  • standard-library/src/Data/List/Fresh/Relation/Unary/All
  • standard-library/src/Data/List/Fresh/Relation/Unary/All/Properties.agda
  • standard-library/src/Data/List/Fresh/Properties.agda
  • standard-library/src/Data/List/Fresh/NonEmpty.agda
  • standard-library/src/Data/List/Fresh/Membership
  • standard-library/src/Data/List/Fresh/Membership/Setoid.agda
  • standard-library/src/Data/List/Fresh/Membership/Setoid
  • standard-library/src/Data/List/Fresh/Membership/Setoid/Properties.agda
  • standard-library/src/Data/List/Extrema.agda
  • standard-library/src/Data/List/Extrema
  • standard-library/src/Data/List/Extrema/Nat.agda
  • standard-library/src/Data/List/Extrema/Core.agda
  • standard-library/src/Data/List/Effectful.agda
  • standard-library/src/Data/List/Effectful
  • standard-library/src/Data/List/Effectful/Transformer.agda
  • standard-library/src/Data/List/Countdown.agda
  • standard-library/src/Data/List/Categorical.agda
  • standard-library/src/Data/List/Categorical
  • standard-library/src/Data/List/Categorical/Transformer.agda
  • standard-library/src/Data/List/Base.agda
  • standard-library/src/Data/Irrelevant.agda
  • standard-library/src/Data/Integer.agda
  • standard-library/src/Data/Integer
  • standard-library/src/Data/Integer/Tactic
  • standard-library/src/Data/Integer/Tactic/RingSolver.agda
  • standard-library/src/Data/Integer/Solver.agda
  • standard-library/src/Data/Integer/Show.agda
  • standard-library/src/Data/Integer/Properties.agda
  • standard-library/src/Data/Integer/Properties
  • standard-library/src/Data/Integer/Properties/NatLemmas.agda
  • standard-library/src/Data/Integer/Literals.agda
  • standard-library/src/Data/Integer/LCM.agda
  • standard-library/src/Data/Integer/Instances.agda
  • standard-library/src/Data/Integer/GCD.agda
  • standard-library/src/Data/Integer/Divisibility.agda
  • standard-library/src/Data/Integer/Divisibility
  • standard-library/src/Data/Integer/Divisibility/Signed.agda
  • standard-library/src/Data/Integer/DivMod.agda
  • standard-library/src/Data/Integer/Coprimality.agda
  • standard-library/src/Data/Integer/Base.agda
  • standard-library/src/Data/Graph
  • standard-library/src/Data/Graph/Acyclic.agda
  • standard-library/src/Data/Float.agda
  • standard-library/src/Data/Float
  • standard-library/src/Data/Float/Properties.agda
  • standard-library/src/Data/Float/Instances.agda
  • standard-library/src/Data/Float/Base.agda
  • standard-library/src/Data/Fin.agda
  • standard-library/src/Data/Fin
  • standard-library/src/Data/Fin/Substitution.agda
  • standard-library/src/Data/Fin/Substitution
  • standard-library/src/Data/Fin/Substitution/List.agda
  • standard-library/src/Data/Fin/Substitution/Lemmas.agda
  • standard-library/src/Data/Fin/Substitution/Example.agda
  • standard-library/src/Data/Fin/Subset.agda
  • standard-library/src/Data/Fin/Subset
  • standard-library/src/Data/Fin/Subset/Properties.agda
  • standard-library/src/Data/Fin/Subset/Induction.agda
  • standard-library/src/Data/Fin/Show.agda
  • standard-library/src/Data/Fin/Relation
  • standard-library/src/Data/Fin/Relation/Unary
  • standard-library/src/Data/Fin/Relation/Unary/Top.agda
  • standard-library/src/Data/Fin/Reflection.agda
  • standard-library/src/Data/Fin/Properties.agda
  • standard-library/src/Data/Fin/Permutation.agda
  • standard-library/src/Data/Fin/Permutation
  • standard-library/src/Data/Fin/Permutation/Transposition
  • standard-library/src/Data/Fin/Permutation/Transposition/List.agda
  • standard-library/src/Data/Fin/Permutation/Components.agda
  • standard-library/src/Data/Fin/Patterns.agda
  • standard-library/src/Data/Fin/Literals.agda
  • standard-library/src/Data/Fin/Instances.agda
  • standard-library/src/Data/Fin/Induction.agda
  • standard-library/src/Data/Fin/Base.agda
  • standard-library/src/Data/Erased.agda
  • standard-library/src/Data/Empty.agda
  • standard-library/src/Data/Empty
  • standard-library/src/Data/Empty/Polymorphic.agda
  • standard-library/src/Data/Empty/Irrelevant.agda
  • standard-library/src/Data/Digit.agda
  • standard-library/src/Data/Digit
  • standard-library/src/Data/Digit/Properties.agda
  • standard-library/src/Data/DifferenceVec.agda
  • standard-library/src/Data/DifferenceNat.agda
  • standard-library/src/Data/DifferenceList.agda
  • standard-library/src/Data/Default.agda
  • standard-library/src/Data/Container.agda
  • standard-library/src/Data/Container
  • standard-library/src/Data/Container/Relation
  • standard-library/src/Data/Container/Relation/Unary
  • standard-library/src/Data/Container/Relation/Unary/Any.agda
  • standard-library/src/Data/Container/Relation/Unary/Any
  • standard-library/src/Data/Container/Relation/Unary/Any/Properties.agda
  • standard-library/src/Data/Container/Relation/Unary/All.agda
  • standard-library/src/Data/Container/Relation/Binary
  • standard-library/src/Data/Container/Relation/Binary/Pointwise.agda
  • standard-library/src/Data/Container/Relation/Binary/Pointwise
  • standard-library/src/Data/Container/Relation/Binary/Pointwise/Properties.agda
  • standard-library/src/Data/Container/Relation/Binary/Equality
  • standard-library/src/Data/Container/Relation/Binary/Equality/Setoid.agda
  • standard-library/src/Data/Container/Related.agda
  • standard-library/src/Data/Container/Properties.agda
  • standard-library/src/Data/Container/Morphism.agda
  • standard-library/src/Data/Container/Morphism
  • standard-library/src/Data/Container/Morphism/Properties.agda
  • standard-library/src/Data/Container/Membership.agda
  • standard-library/src/Data/Container/Indexed.agda
  • standard-library/src/Data/Container/Indexed
  • standard-library/src/Data/Container/Indexed/WithK.agda
  • standard-library/src/Data/Container/Indexed/Relation
  • standard-library/src/Data/Container/Indexed/Relation/Binary
  • standard-library/src/Data/Container/Indexed/Relation/Binary/Pointwise.agda
  • standard-library/src/Data/Container/Indexed/Relation/Binary/Pointwise
  • standard-library/src/Data/Container/Indexed/Relation/Binary/Pointwise/Properties.agda
  • standard-library/src/Data/Container/Indexed/Relation/Binary/Equality
  • standard-library/src/Data/Container/Indexed/Relation/Binary/Equality/Setoid.agda
  • standard-library/src/Data/Container/Indexed/FreeMonad.agda
  • standard-library/src/Data/Container/Indexed/Fixpoints
  • standard-library/src/Data/Container/Indexed/Fixpoints/Guarded.agda
  • standard-library/src/Data/Container/Indexed/Core.agda
  • standard-library/src/Data/Container/Indexed/Combinator.agda
  • standard-library/src/Data/Container/FreeMonad.agda
  • standard-library/src/Data/Container/Fixpoints
  • standard-library/src/Data/Container/Fixpoints/Sized.agda
  • standard-library/src/Data/Container/Fixpoints/Guarded.agda
  • standard-library/src/Data/Container/Core.agda
  • standard-library/src/Data/Container/Combinator.agda
  • standard-library/src/Data/Container/Combinator
  • standard-library/src/Data/Container/Combinator/Properties.agda
  • standard-library/src/Data/Container/Any.agda
  • standard-library/src/Data/Char.agda
  • standard-library/src/Data/Char
  • standard-library/src/Data/Char/Properties.agda
  • standard-library/src/Data/Char/Instances.agda
  • standard-library/src/Data/Char/Base.agda
  • standard-library/src/Data/Bytestring
  • standard-library/src/Data/Bytestring/Primitive.agda
  • standard-library/src/Data/Bytestring/IO.agda
  • standard-library/src/Data/Bytestring/IO
  • standard-library/src/Data/Bytestring/IO/Primitive.agda
  • standard-library/src/Data/Bytestring/Builder
  • standard-library/src/Data/Bytestring/Builder/Primitive.agda
  • standard-library/src/Data/Bytestring/Builder/Base.agda
  • standard-library/src/Data/Bytestring/Base.agda
  • standard-library/src/Data/Bool.agda
  • standard-library/src/Data/Bool
  • standard-library/src/Data/Bool/Solver.agda
  • standard-library/src/Data/Bool/Show.agda
  • standard-library/src/Data/Bool/Properties.agda
  • standard-library/src/Data/Bool/Instances.agda
  • standard-library/src/Data/Bool/Base.agda
  • standard-library/src/Data/AVL.agda
  • standard-library/src/Data/AVL
  • standard-library/src/Data/AVL/Value.agda
  • standard-library/src/Data/AVL/Sets.agda
  • standard-library/src/Data/AVL/NonEmpty.agda
  • standard-library/src/Data/AVL/NonEmpty
  • standard-library/src/Data/AVL/NonEmpty/Propositional.agda
  • standard-library/src/Data/AVL/Map.agda
  • standard-library/src/Data/AVL/Key.agda
  • standard-library/src/Data/AVL/IndexedMap.agda
  • standard-library/src/Data/AVL/Indexed.agda
  • standard-library/src/Data/AVL/Indexed
  • standard-library/src/Data/AVL/Indexed/WithK.agda
  • standard-library/src/Data/AVL/Height.agda
  • standard-library/src/Codata
  • standard-library/src/Codata/Sized
  • standard-library/src/Codata/Sized/Thunk.agda
  • standard-library/src/Codata/Sized/Stream.agda
  • standard-library/src/Codata/Sized/Stream
  • standard-library/src/Codata/Sized/Stream/Properties.agda
  • standard-library/src/Codata/Sized/Stream/Instances.agda
  • standard-library/src/Codata/Sized/Stream/Effectful.agda
  • standard-library/src/Codata/Sized/Stream/Categorical.agda
  • standard-library/src/Codata/Sized/Stream/Bisimilarity.agda
  • standard-library/src/Codata/Sized/M.agda
  • standard-library/src/Codata/Sized/M
  • standard-library/src/Codata/Sized/M/Properties.agda
  • standard-library/src/Codata/Sized/M/Bisimilarity.agda
  • standard-library/src/Codata/Sized/Delay.agda
  • standard-library/src/Codata/Sized/Delay
  • standard-library/src/Codata/Sized/Delay/Properties.agda
  • standard-library/src/Codata/Sized/Delay/Effectful.agda
  • standard-library/src/Codata/Sized/Delay/Categorical.agda
  • standard-library/src/Codata/Sized/Delay/Bisimilarity.agda
  • standard-library/src/Codata/Sized/Cowriter.agda
  • standard-library/src/Codata/Sized/Cowriter
  • standard-library/src/Codata/Sized/Cowriter/Bisimilarity.agda
  • standard-library/src/Codata/Sized/Covec.agda
  • standard-library/src/Codata/Sized/Covec
  • standard-library/src/Codata/Sized/Covec/Properties.agda
  • standard-library/src/Codata/Sized/Covec/Instances.agda
  • standard-library/src/Codata/Sized/Covec/Effectful.agda
  • standard-library/src/Codata/Sized/Covec/Categorical.agda
  • standard-library/src/Codata/Sized/Covec/Bisimilarity.agda
  • standard-library/src/Codata/Sized/Conat.agda
  • standard-library/src/Codata/Sized/Conat
  • standard-library/src/Codata/Sized/Conat/Properties.agda
  • standard-library/src/Codata/Sized/Conat/Literals.agda
  • standard-library/src/Codata/Sized/Conat/Bisimilarity.agda
  • standard-library/src/Codata/Sized/Colist.agda
  • standard-library/src/Codata/Sized/Colist
  • standard-library/src/Codata/Sized/Colist/Properties.agda
  • standard-library/src/Codata/Sized/Colist/Effectful.agda
  • standard-library/src/Codata/Sized/Colist/Categorical.agda
  • standard-library/src/Codata/Sized/Colist/Bisimilarity.agda
  • standard-library/src/Codata/Sized/Cofin.agda
  • standard-library/src/Codata/Sized/Cofin
  • standard-library/src/Codata/Sized/Cofin/Literals.agda
  • standard-library/src/Codata/Musical
  • standard-library/src/Codata/Musical/Stream.agda
  • standard-library/src/Codata/Musical/Notation.agda
  • standard-library/src/Codata/Musical/M.agda
  • standard-library/src/Codata/Musical/M
  • standard-library/src/Codata/Musical/M/Indexed.agda
  • standard-library/src/Codata/Musical/Covec.agda
  • standard-library/src/Codata/Musical/Costring.agda
  • standard-library/src/Codata/Musical/Conversion.agda
  • standard-library/src/Codata/Musical/Conat.agda
  • standard-library/src/Codata/Musical/Conat
  • standard-library/src/Codata/Musical/Conat/Base.agda
  • standard-library/src/Codata/Musical/Colist.agda
  • standard-library/src/Codata/Musical/Colist
  • standard-library/src/Codata/Musical/Colist/Relation
  • standard-library/src/Codata/Musical/Colist/Relation/Unary
  • standard-library/src/Codata/Musical/Colist/Relation/Unary/Any.agda
  • standard-library/src/Codata/Musical/Colist/Relation/Unary/Any
  • standard-library/src/Codata/Musical/Colist/Relation/Unary/Any/Properties.agda
  • standard-library/src/Codata/Musical/Colist/Relation/Unary/All.agda
  • standard-library/src/Codata/Musical/Colist/Relation/Unary/All
  • standard-library/src/Codata/Musical/Colist/Relation/Unary/All/Properties.agda
  • standard-library/src/Codata/Musical/Colist/Properties.agda
  • standard-library/src/Codata/Musical/Colist/Infinite-merge.agda
  • standard-library/src/Codata/Musical/Colist/Bisimilarity.agda
  • standard-library/src/Codata/Musical/Colist/Base.agda
  • standard-library/src/Codata/Musical/Cofin.agda
  • standard-library/src/Codata/Guarded
  • standard-library/src/Codata/Guarded/Stream.agda
  • standard-library/src/Codata/Guarded/Stream
  • standard-library/src/Codata/Guarded/Stream/Relation
  • standard-library/src/Codata/Guarded/Stream/Relation/Unary
  • standard-library/src/Codata/Guarded/Stream/Relation/Unary/Any.agda
  • standard-library/src/Codata/Guarded/Stream/Relation/Unary/All.agda
  • standard-library/src/Codata/Guarded/Stream/Relation/Binary
  • standard-library/src/Codata/Guarded/Stream/Relation/Binary/Pointwise.agda
  • standard-library/src/Codata/Guarded/Stream/Properties.agda
  • standard-library/src/Codata/Guarded/M.agda
  • standard-library/src/Axiom
  • standard-library/src/Axiom/UniquenessOfIdentityProofs.agda
  • standard-library/src/Axiom/UniquenessOfIdentityProofs
  • standard-library/src/Axiom/UniquenessOfIdentityProofs/WithK.agda
  • standard-library/src/Axiom/Extensionality
  • standard-library/src/Axiom/Extensionality/Propositional.agda
  • standard-library/src/Axiom/Extensionality/Heterogeneous.agda
  • standard-library/src/Axiom/ExcludedMiddle.agda
  • standard-library/src/Axiom/DoubleNegationElimination.agda
  • standard-library/src/Algebra.agda
  • standard-library/src/Algebra
  • standard-library/src/Algebra/Structures.agda
  • standard-library/src/Algebra/Structures
  • standard-library/src/Algebra/Structures/Biased.agda
  • standard-library/src/Algebra/Solver
  • standard-library/src/Algebra/Solver/Ring.agda
  • standard-library/src/Algebra/Solver/Ring
  • standard-library/src/Algebra/Solver/Ring/Simple.agda
  • standard-library/src/Algebra/Solver/Ring/NaturalCoefficients.agda
  • standard-library/src/Algebra/Solver/Ring/NaturalCoefficients
  • standard-library/src/Algebra/Solver/Ring/NaturalCoefficients/Default.agda
  • standard-library/src/Algebra/Solver/Ring/Lemmas.agda
  • standard-library/src/Algebra/Solver/Ring/AlmostCommutativeRing.agda
  • standard-library/src/Algebra/Solver/Monoid.agda
  • standard-library/src/Algebra/Solver/IdempotentCommutativeMonoid.agda
  • standard-library/src/Algebra/Solver/IdempotentCommutativeMonoid
  • standard-library/src/Algebra/Solver/IdempotentCommutativeMonoid/Example.agda
  • standard-library/src/Algebra/Solver/CommutativeMonoid.agda
  • standard-library/src/Algebra/Solver/CommutativeMonoid
  • standard-library/src/Algebra/Solver/CommutativeMonoid/Example.agda
  • standard-library/src/Algebra/Properties
  • standard-library/src/Algebra/Properties/Semiring
  • standard-library/src/Algebra/Properties/Semiring/Sum.agda
  • standard-library/src/Algebra/Properties/Semiring/Primality.agda
  • standard-library/src/Algebra/Properties/Semiring/Mult.agda
  • standard-library/src/Algebra/Properties/Semiring/Mult
  • standard-library/src/Algebra/Properties/Semiring/Mult/TCOptimised.agda
  • standard-library/src/Algebra/Properties/Semiring/Exp.agda
  • standard-library/src/Algebra/Properties/Semiring/Exp
  • standard-library/src/Algebra/Properties/Semiring/Exp/TailRecursiveOptimised.agda
  • standard-library/src/Algebra/Properties/Semiring/Exp/TCOptimised.agda
  • standard-library/src/Algebra/Properties/Semiring/Divisibility.agda
  • standard-library/src/Algebra/Properties/Semiring/Binomial.agda
  • standard-library/src/Algebra/Properties/Semilattice.agda
  • standard-library/src/Algebra/Properties/Semigroup.agda
  • standard-library/src/Algebra/Properties/Semigroup
  • standard-library/src/Algebra/Properties/Semigroup/Divisibility.agda
  • standard-library/src/Algebra/Properties/RingWithoutOne.agda
  • standard-library/src/Algebra/Properties/Ring.agda
  • standard-library/src/Algebra/Properties/Quasigroup.agda
  • standard-library/src/Algebra/Properties/MoufangLoop.agda
  • standard-library/src/Algebra/Properties/Monoid
  • standard-library/src/Algebra/Properties/Monoid/Sum.agda
  • standard-library/src/Algebra/Properties/Monoid/Mult.agda
  • standard-library/src/Algebra/Properties/Monoid/Mult
  • standard-library/src/Algebra/Properties/Monoid/Mult/TCOptimised.agda
  • standard-library/src/Algebra/Properties/Monoid/Divisibility.agda
  • standard-library/src/Algebra/Properties/MiddleBolLoop.agda
  • standard-library/src/Algebra/Properties/Magma
  • standard-library/src/Algebra/Properties/Magma/Divisibility.agda
  • standard-library/src/Algebra/Properties/Loop.agda
  • standard-library/src/Algebra/Properties/Lattice.agda
  • standard-library/src/Algebra/Properties/KleeneAlgebra.agda
  • standard-library/src/Algebra/Properties/Group.agda
  • standard-library/src/Algebra/Properties/DistributiveLattice.agda
  • standard-library/src/Algebra/Properties/CommutativeSemiring
  • standard-library/src/Algebra/Properties/CommutativeSemiring/Exp.agda
  • standard-library/src/Algebra/Properties/CommutativeSemiring/Exp
  • standard-library/src/Algebra/Properties/CommutativeSemiring/Exp/TCOptimised.agda
  • standard-library/src/Algebra/Properties/CommutativeSemiring/Binomial.agda
  • standard-library/src/Algebra/Properties/CommutativeSemigroup.agda
  • standard-library/src/Algebra/Properties/CommutativeSemigroup
  • standard-library/src/Algebra/Properties/CommutativeSemigroup/Divisibility.agda
  • standard-library/src/Algebra/Properties/CommutativeMonoid.agda
  • standard-library/src/Algebra/Properties/CommutativeMonoid
  • standard-library/src/Algebra/Properties/CommutativeMonoid/Sum.agda
  • standard-library/src/Algebra/Properties/CommutativeMonoid/Mult.agda
  • standard-library/src/Algebra/Properties/CommutativeMonoid/Mult
  • standard-library/src/Algebra/Properties/CommutativeMonoid/Mult/TCOptimised.agda
  • standard-library/src/Algebra/Properties/CommutativeMagma
  • standard-library/src/Algebra/Properties/CommutativeMagma/Divisibility.agda
  • standard-library/src/Algebra/Properties/CancellativeCommutativeSemiring.agda
  • standard-library/src/Algebra/Properties/BooleanAlgebra.agda
  • standard-library/src/Algebra/Properties/BooleanAlgebra
  • standard-library/src/Algebra/Properties/BooleanAlgebra/Expression.agda
  • standard-library/src/Algebra/Properties/AbelianGroup.agda
  • standard-library/src/Algebra/Operations
  • standard-library/src/Algebra/Operations/Semiring.agda
  • standard-library/src/Algebra/Operations/Ring.agda
  • standard-library/src/Algebra/Operations/CommutativeMonoid.agda
  • standard-library/src/Algebra/Morphism.agda
  • standard-library/src/Algebra/Morphism
  • standard-library/src/Algebra/Morphism/Structures.agda
  • standard-library/src/Algebra/Morphism/RingMonomorphism.agda
  • standard-library/src/Algebra/Morphism/MonoidMonomorphism.agda
  • standard-library/src/Algebra/Morphism/MagmaMonomorphism.agda
  • standard-library/src/Algebra/Morphism/GroupMonomorphism.agda
  • standard-library/src/Algebra/Morphism/Definitions.agda
  • standard-library/src/Algebra/Morphism/Construct
  • standard-library/src/Algebra/Morphism/Construct/Terminal.agda
  • standard-library/src/Algebra/Morphism/Construct/Initial.agda
  • standard-library/src/Algebra/Morphism/Construct/Identity.agda
  • standard-library/src/Algebra/Morphism/Construct/Composition.agda
  • standard-library/src/Algebra/Morphism/Consequences.agda
  • standard-library/src/Algebra/Module.agda
  • standard-library/src/Algebra/Module
  • standard-library/src/Algebra/Module/Structures.agda
  • standard-library/src/Algebra/Module/Structures
  • standard-library/src/Algebra/Module/Structures/Biased.agda
  • standard-library/src/Algebra/Module/Properties.agda
  • standard-library/src/Algebra/Module/Properties
  • standard-library/src/Algebra/Module/Properties/Semimodule.agda
  • standard-library/src/Algebra/Module/Morphism
  • standard-library/src/Algebra/Module/Morphism/Structures.agda
  • standard-library/src/Algebra/Module/Morphism/ModuleHomomorphism.agda
  • standard-library/src/Algebra/Module/Morphism/Definitions.agda
  • standard-library/src/Algebra/Module/Morphism/Construct
  • standard-library/src/Algebra/Module/Morphism/Construct/Identity.agda
  • standard-library/src/Algebra/Module/Morphism/Construct/Composition.agda
  • standard-library/src/Algebra/Module/Definitions.agda
  • standard-library/src/Algebra/Module/Definitions
  • standard-library/src/Algebra/Module/Definitions/Right.agda
  • standard-library/src/Algebra/Module/Definitions/Left.agda
  • standard-library/src/Algebra/Module/Definitions/Bi.agda
  • standard-library/src/Algebra/Module/Definitions/Bi
  • standard-library/src/Algebra/Module/Definitions/Bi/Simultaneous.agda
  • standard-library/src/Algebra/Module/Core.agda
  • standard-library/src/Algebra/Module/Construct
  • standard-library/src/Algebra/Module/Construct/Zero.agda
  • standard-library/src/Algebra/Module/Construct/TensorUnit.agda
  • standard-library/src/Algebra/Module/Construct/Idealization.agda
  • standard-library/src/Algebra/Module/Construct/DirectProduct.agda
  • standard-library/src/Algebra/Module/Consequences.agda
  • standard-library/src/Algebra/Module/Bundles.agda
  • standard-library/src/Algebra/Module/Bundles
  • standard-library/src/Algebra/Module/Bundles/Raw.agda
  • standard-library/src/Algebra/Lattice.agda
  • standard-library/src/Algebra/Lattice
  • standard-library/src/Algebra/Lattice/Structures.agda
  • standard-library/src/Algebra/Lattice/Structures
  • standard-library/src/Algebra/Lattice/Structures/Biased.agda
  • standard-library/src/Algebra/Lattice/Properties
  • standard-library/src/Algebra/Lattice/Properties/Semilattice.agda
  • standard-library/src/Algebra/Lattice/Properties/Lattice.agda
  • standard-library/src/Algebra/Lattice/Properties/DistributiveLattice.agda
  • standard-library/src/Algebra/Lattice/Properties/BooleanAlgebra.agda
  • standard-library/src/Algebra/Lattice/Properties/BooleanAlgebra
  • standard-library/src/Algebra/Lattice/Properties/BooleanAlgebra/Expression.agda
  • standard-library/src/Algebra/Lattice/Morphism.agda
  • standard-library/src/Algebra/Lattice/Morphism
  • standard-library/src/Algebra/Lattice/Morphism/Structures.agda
  • standard-library/src/Algebra/Lattice/Morphism/LatticeMonomorphism.agda
  • standard-library/src/Algebra/Lattice/Morphism/Construct
  • standard-library/src/Algebra/Lattice/Morphism/Construct/Identity.agda
  • standard-library/src/Algebra/Lattice/Morphism/Construct/Composition.agda
  • standard-library/src/Algebra/Lattice/Construct
  • standard-library/src/Algebra/Lattice/Construct/Zero.agda
  • standard-library/src/Algebra/Lattice/Construct/Subst
  • standard-library/src/Algebra/Lattice/Construct/Subst/Equality.agda
  • standard-library/src/Algebra/Lattice/Construct/NaturalChoice
  • standard-library/src/Algebra/Lattice/Construct/NaturalChoice/MinOp.agda
  • standard-library/src/Algebra/Lattice/Construct/NaturalChoice/MinMaxOp.agda
  • standard-library/src/Algebra/Lattice/Construct/NaturalChoice/MaxOp.agda
  • standard-library/src/Algebra/Lattice/Construct/LiftedChoice.agda
  • standard-library/src/Algebra/Lattice/Construct/DirectProduct.agda
  • standard-library/src/Algebra/Lattice/Bundles.agda
  • standard-library/src/Algebra/Lattice/Bundles
  • standard-library/src/Algebra/Lattice/Bundles/Raw.agda
  • standard-library/src/Algebra/FunctionProperties
  • standard-library/src/Algebra/FunctionProperties/Consequences.agda
  • standard-library/src/Algebra/FunctionProperties/Consequences
  • standard-library/src/Algebra/FunctionProperties/Consequences/Propositional.agda
  • standard-library/src/Algebra/FunctionProperties/Consequences/Core.agda
  • standard-library/src/Algebra/Definitions.agda
  • standard-library/src/Algebra/Definitions
  • standard-library/src/Algebra/Definitions/RawSemiring.agda
  • standard-library/src/Algebra/Definitions/RawMonoid.agda
  • standard-library/src/Algebra/Definitions/RawMagma.agda
  • standard-library/src/Algebra/Core.agda
  • standard-library/src/Algebra/Construct
  • standard-library/src/Algebra/Construct/Zero.agda
  • standard-library/src/Algebra/Construct/Terminal.agda
  • standard-library/src/Algebra/Construct/Subst
  • standard-library/src/Algebra/Construct/Subst/Equality.agda
  • standard-library/src/Algebra/Construct/Pointwise.agda
  • standard-library/src/Algebra/Construct/NaturalChoice
  • standard-library/src/Algebra/Construct/NaturalChoice/MinOp.agda
  • standard-library/src/Algebra/Construct/NaturalChoice/MinMaxOp.agda
  • standard-library/src/Algebra/Construct/NaturalChoice/Min.agda
  • standard-library/src/Algebra/Construct/NaturalChoice/MaxOp.agda
  • standard-library/src/Algebra/Construct/NaturalChoice/Max.agda
  • standard-library/src/Algebra/Construct/NaturalChoice/Base.agda
  • standard-library/src/Algebra/Construct/LiftedChoice.agda
  • standard-library/src/Algebra/Construct/LexProduct.agda
  • standard-library/src/Algebra/Construct/LexProduct
  • standard-library/src/Algebra/Construct/LexProduct/Inner.agda
  • standard-library/src/Algebra/Construct/LexProduct/Base.agda
  • standard-library/src/Algebra/Construct/Initial.agda
  • standard-library/src/Algebra/Construct/Flip
  • standard-library/src/Algebra/Construct/Flip/Op.agda
  • standard-library/src/Algebra/Construct/DirectProduct.agda
  • standard-library/src/Algebra/Construct/Add
  • standard-library/src/Algebra/Construct/Add/Identity.agda
  • standard-library/src/Algebra/Consequences
  • standard-library/src/Algebra/Consequences/Setoid.agda
  • standard-library/src/Algebra/Consequences/Propositional.agda
  • standard-library/src/Algebra/Consequences/Base.agda
  • standard-library/src/Algebra/Bundles.agda
  • standard-library/src/Algebra/Bundles
  • standard-library/src/Algebra/Bundles/Raw.agda
  • standard-library/src/Algebra/Apartness.agda
  • standard-library/src/Algebra/Apartness
  • standard-library/src/Algebra/Apartness/Structures.agda
  • standard-library/src/Algebra/Apartness/Properties
  • standard-library/src/Algebra/Apartness/Properties/HeytingCommutativeRing.agda
  • standard-library/src/Algebra/Apartness/Bundles.agda
  • standard-library/publish-listings.sh
  • standard-library/graph.sh
  • standard-library/fix-whitespace.yaml
  • standard-library/doc
  • standard-library/doc/updating-experimental.txt
  • standard-library/doc/style-guide.md
  • standard-library/doc/standard-library-doc.agda-lib
  • standard-library/doc/release-guide.txt
  • standard-library/doc/installation-guide.md
  • standard-library/doc/README.agda
  • standard-library/doc/README
  • standard-library/doc/README/Text
  • standard-library/doc/README/Text/Tabular.agda
  • standard-library/doc/README/Text/Regex.agda
  • standard-library/doc/README/Text/Printf.agda
  • standard-library/doc/README/Text/Pretty.agda
  • standard-library/doc/README/Tactic
  • standard-library/doc/README/Tactic/RingSolver.agda
  • standard-library/doc/README/Tactic/MonoidSolver.agda
  • standard-library/doc/README/Tactic/Cong.agda
  • standard-library/doc/README/Relation
  • standard-library/doc/README/Relation/Binary
  • standard-library/doc/README/Relation/Binary/TypeClasses.agda
  • standard-library/doc/README/Reflection
  • standard-library/doc/README/Reflection/External.agda
  • standard-library/doc/README/Nary.agda
  • standard-library/doc/README/Inspect.agda
  • standard-library/doc/README/IO.agda
  • standard-library/doc/README/Function
  • standard-library/doc/README/Function/Reasoning.agda
  • standard-library/doc/README/Foreign
  • standard-library/doc/README/Foreign/Haskell.agda
  • standard-library/doc/README/Effect
  • standard-library/doc/README/Effect/Monad
  • standard-library/doc/README/Effect/Monad/Partiality.agda
  • standard-library/doc/README/Design
  • standard-library/doc/README/Design/LevelPolymorphism.md
  • standard-library/doc/README/Design/Hierarchies.agda
  • standard-library/doc/README/Design/Fixity.agda
  • standard-library/doc/README/Design/Decidability.agda
  • standard-library/doc/README/Debug
  • standard-library/doc/README/Debug/Trace.agda
  • standard-library/doc/README/Data.agda
  • standard-library/doc/README/Data
  • standard-library/doc/README/Data/Wrap.agda
  • standard-library/doc/README/Data/Vec
  • standard-library/doc/README/Data/Vec/Relation
  • standard-library/doc/README/Data/Vec/Relation/Binary
  • standard-library/doc/README/Data/Vec/Relation/Binary/Equality
  • standard-library/doc/README/Data/Vec/Relation/Binary/Equality/Cast.agda
  • standard-library/doc/README/Data/Trie
  • standard-library/doc/README/Data/Trie/NonDependent.agda
  • standard-library/doc/README/Data/Tree
  • standard-library/doc/README/Data/Tree/Rose.agda
  • standard-library/doc/README/Data/Tree/Binary.agda
  • standard-library/doc/README/Data/Tree/AVL.agda
  • standard-library/doc/README/Data/Record.agda
  • standard-library/doc/README/Data/Nat.agda
  • standard-library/doc/README/Data/Nat
  • standard-library/doc/README/Data/Nat/Induction.agda
  • standard-library/doc/README/Data/List.agda
  • standard-library/doc/README/Data/List
  • standard-library/doc/README/Data/List/Relation
  • standard-library/doc/README/Data/List/Relation/Unary
  • standard-library/doc/README/Data/List/Relation/Unary/Any.agda
  • standard-library/doc/README/Data/List/Relation/Unary/All.agda
  • standard-library/doc/README/Data/List/Relation/Ternary
  • standard-library/doc/README/Data/List/Relation/Ternary/Interleaving.agda
  • standard-library/doc/README/Data/List/Relation/Binary
  • standard-library/doc/README/Data/List/Relation/Binary/Subset.agda
  • standard-library/doc/README/Data/List/Relation/Binary/Pointwise.agda
  • standard-library/doc/README/Data/List/Relation/Binary/Permutation.agda
  • standard-library/doc/README/Data/List/Relation/Binary/Equality.agda
  • standard-library/doc/README/Data/List/Membership.agda
  • standard-library/doc/README/Data/List/Fresh.agda
  • standard-library/doc/README/Data/Integer.agda
  • standard-library/doc/README/Data/Fin
  • standard-library/doc/README/Data/Fin/Substitution
  • standard-library/doc/README/Data/Fin/Substitution/UntypedLambda.agda
  • standard-library/doc/README/Data/Fin/Relation
  • standard-library/doc/README/Data/Fin/Relation/Unary
  • standard-library/doc/README/Data/Fin/Relation/Unary/Top.agda
  • standard-library/doc/README/Data/Default.agda
  • standard-library/doc/README/Data/Container
  • standard-library/doc/README/Data/Container/Indexed
  • standard-library/doc/README/Data/Container/Indexed/VectorExample.agda
  • standard-library/doc/README/Data/Container/Indexed/MultiSortedAlgebraExample.agda
  • standard-library/doc/README/Data/Container/FreeMonad.agda
  • standard-library/doc/README/Case.agda
  • standard-library/doc/README/Axiom.agda
  • standard-library/dev
  • standard-library/cabal.haskell-ci
  • standard-library/agda-stdlib-utils.cabal
  • standard-library/Setup.hs
  • standard-library/README.md
  • standard-library/LICENCE
  • standard-library/Header
  • standard-library/HACKING.md
  • standard-library/GenerateEverything.hs
  • standard-library/GNUmakefile
  • standard-library/CITATION.cff
  • standard-library/CHANGELOG.md
  • standard-library/CHANGELOG
  • standard-library/CHANGELOG/v2.0.md
  • standard-library/CHANGELOG/v1.7.md
  • standard-library/CHANGELOG/v1.7.3.md
  • standard-library/CHANGELOG/v1.7.2.md
  • standard-library/CHANGELOG/v1.7.1.md
  • standard-library/CHANGELOG/v1.6.md
  • standard-library/CHANGELOG/v1.5.md
  • standard-library/CHANGELOG/v1.4.md
  • standard-library/CHANGELOG/v1.3.md
  • standard-library/CHANGELOG/v1.2.md
  • standard-library/CHANGELOG/v1.1.md
  • standard-library/CHANGELOG/v1.0.md
  • standard-library/CHANGELOG/v1.0.1.md
  • standard-library/CHANGELOG/v0.17.md
  • standard-library/CHANGELOG/v0.16.md
  • standard-library/CHANGELOG/v0.15.md
  • standard-library/CHANGELOG/v0.14.md
  • standard-library/CHANGELOG/v0.13.md
  • standard-library/CHANGELOG/v0.12.md
  • standard-library/CHANGELOG/v0.11.md
  • standard-library/CHANGELOG/v0.10.md
  • standard-library/CHANGELOG/v0.09.md
  • standard-library/CHANGELOG/v0.08.md
  • standard-library/CHANGELOG/v0.08.1.md
  • standard-library/CHANGELOG/v0.07.md
  • standard-library/CHANGELOG/v0.06.md
  • standard-library/CHANGELOG/v0.05.md
  • standard-library/CHANGELOG/v0.04.md
  • standard-library/CHANGELOG/v0.03.md
  • standard-library/CHANGELOG/v0.02.md
  • standard-library/CHANGELOG/v0.01.md
  • standard-library/AllNonAsciiChars.hs
  • standard-library/.mailmap
  • standard-library/.gitignore
  • standard-library/.github
  • standard-library/.github/workflows
  • standard-library/.github/workflows/whitespace.yml
  • standard-library/.github/workflows/haskell-ci.yml
  • standard-library/.github/workflows/ci-ubuntu.yml
  • standard-library/.github/tooling
  • standard-library/.github/tooling/landing.sh
  • standard-library/.github/tooling/landing-top.html
  • standard-library/.github/tooling/landing-bottom.html
  • standard-library/.github/tooling/index.sh
  • standard-library/.github/tooling/index.agda
  • standard-library/.github/haskell-ci.patch
  • standard-library/.gitattributes
  • standard-library/.boring
State: G2JQU4UG7GQPRLDSFIBMRELET6K26KRNRC5WD6VZZBUMAU7WS5OQC
State: ZDCTBTZKVGJO3PLPMJ4ZJG5CAGYTDFMA67XTSPDCO22PBUIQ3EDAC
State: ZDDUSN5OJE5CODEZ7Z2ZVIHBDTIE3CTNZX2KRHAJT2CRSKXYR6JQC
State: 6ENQH6ZDWF5FQGVYN5LVBOJ7PHT3HVI5D2AWYZXV6RUBJDBZJZBAC
State: Y6VCR6I6YGBYX5W2PVTFSLLXPGWK6RBD63A7JMBUHOA7QVZIIH7QC
State: 6P23EQFKX5MWL42PFLSAYPCMJ3TCNKDP6XEBQDLHCEBL5274RVBQC
State: GF3GQDQU5BS7G3KWGK4KOR5JPCQMVXAZD4WCQZSJ24P2V7D72YWAC
State: 2IXCOOKPX2QLFXI4WYH3IP54X6FWMUHBG5AA55WDE3OTYO2S5FEAC
Older