Agda 筆記

雜記/待看

• records

Tutorials

• A Practical Agda Tutorial
• Computer Aided Formal Reasoning
• Agda’s official documentation

Links for stdlib

• /
• /Function.agda
• /Level.agda
• /Function/
  • /Function/Equality.agda
  • /Function/Equivalence.agda
  • /Function/Injection.agda
  • /Function/Surjection.agda
  • /Function/Bijection.agda
• /Relation/
  • /Relation/Nullary.agda
    • /Relation/Nullary/Decidable.agda
  • /Relation/Unary.agda
  • /Relation/Binary.agda
    • /Relation/Binary/Core.agda
    • /Relation/Binary/PropositionalEquality.agda
• /Data/
  • /Data/Empty.agda
  • /Data/Unit.agda
  • /Data/Bool.agda
    • /Data/Bool/Base.agda
  • /Data/Product.agda
  • /Data/Sum.agda
  • /Data/Nat.agda
    • /Data/Nat/Base.agda
  • /Data/Fin.agda
  • /Data/Vec.agda
    • /Data/Vec/Equality.agda
  • /Data/Maybe.agda
    • /Data/Maybe/Base.agda
  • /Data/String.agda
    • /Data/String/Base.agda
  • /Data/List.agda
    • /Data/List/Base.agda
    • /Data/List/Properties.agda
    • /Data/List/NonEmpty.agda
      • /Data/List/NonEmpty/Properties.agda
    • /Data/List/All.agda
      • /Data/List/All/Properties.agda
    • /Data/List/Any.agda
      • /Data/List/Any/Properties.agda
      • /Data/List/Any/Membership.agda