Agda Github Community

All

26 repositories

agda
Public
Agda is a dependently typed programming language / interactive theorem prover.
programming-language dependent-types proof-assistant type-theory agda
Haskell
•
Other
•379•2.7k•991•58•Updated Aug 10, 2025Aug 10, 2025
agda-stdlib
Public
The Agda standard library
library proof agda
Agda
•
Other
•251•620•265•43•Updated Aug 6, 2025Aug 6, 2025
agda-stdlib-classes
Public
Extension of Agda's standard library to accommodate a more typeclass-friendly interface.
Agda
•
MIT License
•3•3•3•3•Updated Aug 5, 2025Aug 5, 2025
agda-stdlib-meta
Public
Meta-programming utilities for Agda.
Agda
•
MIT License
•4•19•9•2•Updated Aug 5, 2025Aug 5, 2025
cubical
Public
An experimental library for Cubical Agda
library cubical-type-theory agda
Agda
•
Other
•154•498•66•46•Updated Aug 4, 2025Aug 4, 2025
agda-categories
Public
A new Categories library for Agda
Agda
•
MIT License
•71•384•52•15•Updated Aug 3, 2025Aug 3, 2025
tasty-silver
Public
A fancy test runner for tasty and support for golden tests.
Haskell
•
MIT License
•3•13•8•0•Updated Jul 30, 2025Jul 30, 2025
agda2hs
Public
Compiling Agda code to readable Haskell
Agda
•
MIT License
•42•190•62•9•Updated Jul 30, 2025Jul 30, 2025
agda-language-server
Public
Language Server for Agda
agda language-server-protocol agda-mode
Haskell
•
MIT License
•18•113•10•0•Updated Jul 29, 2025Jul 29, 2025
cornelis
Public
agda-mode for neovim
agda vim-textobj-user nvim-hs vim-which-key neovim
Haskell
•
BSD 3-Clause "New" or "Revised" License
•24•162•20•2•Updated Jul 25, 2025Jul 25, 2025
fix-whitespace
Public
Fixes whitespace issues
sanitization formatter version-control whitespace
Haskell
•
Other
•7•8•5•1•Updated Jul 23, 2025Jul 23, 2025
agda-pretty
Public
Agda port of the Haskell pretty (Text.PrettyPrint) package
Agda
•
Other
•0•1•0•0•Updated Jun 25, 2025Jun 25, 2025
ooAgda
Public
Interactive and object-oriented programming in Agda using coinductive types
Agda
•
MIT License
•2•23•0•1•Updated Jun 2, 2025Jun 2, 2025
agda2lambox
Public
Compiling Agda's internal syntax to λ-box terms.
Haskell
•
Other
•2•6•11•3•Updated Feb 5, 2025Feb 5, 2025
nix-packages
Public
Packages and abstractions to use Nix as a package manager for Agda
Nix
•
MIT License
•0•1•0•0•Updated Nov 26, 2024Nov 26, 2024
organization
Public
The Agda organization itself
0•2•1•0•Updated Nov 23, 2024Nov 23, 2024
agda-base
Public
This is an experimental base library which is supposed to contain functional datastructures and reflection code.
Agda
•
Other
•0•11•1•0•Updated Jun 6, 2023Jun 6, 2023
hs-tags
Public
Generate ctags and etags for Haskell files
Haskell
•
Other
•1•5•3•0•Updated Mar 28, 2023Mar 28, 2023
agda-finite-prover
Public
Library for proving propositions quantified over finite sets
Agda
•2•14•2•0•Updated Sep 21, 2022Sep 21, 2022
guarded
Public
Agda
•1•5•0•0•Updated Feb 3, 2022Feb 3, 2022
agda-pkg
Public
apkg - package manager for Agda
package-manager lightweight-dependency-management agda
Python
•
Other
•8•38•2•2•Updated Jul 17, 2021Jul 17, 2021
categories-examples
Public
Examples of categorical structures
Agda
•
MIT License
•4•11•2•1•Updated Mar 19, 2021Mar 19, 2021
package-index
Public
A package Index for agda libraries
package-index apkg agda agda-pkg
2•12•3•1•Updated Mar 14, 2021Mar 14, 2021
agda-spec
Public
Specification of Agda.
TeX
•
The Unlicense
•3•25•1•0•Updated Jan 13, 2019Jan 13, 2019
agda-ocaml
Public
OCaml backend for Agda
Haskell
•
BSD 3-Clause "New" or "Revised" License
•6•40•1•0•Updated Oct 4, 2018Oct 4, 2018
agda-ghc-names
Public
Tool for making sense of the Haskell code generated by the Agda compiler
Haskell
•
MIT License
•2•4•0•0•Updated Mar 23, 2017Mar 23, 2017