multiset VS Agda

Compare multiset vs Agda and see what are their differences.


multiset haskell package (by twanvl)


Agda is a dependently typed programming language / interactive theorem prover. (by agda)
Our great sponsors
  • OPS - Build and Run Open Source Unikernels
  • SonarLint - Deliver Cleaner and Safer Code - Right in Your IDE of Choice!
  • Scout APM - Less time debugging, more time building
multiset Agda
0 5
18 1,714
- 2.6%
0.0 9.7
almost 2 years ago 5 days ago
Haskell Haskell
BSD 3-clause "New" or "Revised" License LicenseRef-OtherLicense
The number of mentions indicates the total number of mentions that we've tracked plus the number of user suggested alternatives.
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.


Posts with mentions or reviews of multiset. We have used some of these posts to build our list of alternatives and similar projects.

We haven't tracked posts mentioning multiset yet.
Tracking mentions began in Dec 2020.


Posts with mentions or reviews of Agda. We have used some of these posts to build our list of alternatives and similar projects. The last one was on 2021-10-18.
  • Integer overflow causes Russel's paradox
    1 project | | 22 Dec 2021
  • What input method would you prefer for Unicode characters in a neovim plugin?
    7 projects | | 18 Oct 2021
    My best guess is that it has not really been maintained lately, there were only 12 commits in the last 7 years, some of which are just global modifications, which include this file as well:
  • Type in type and HoTT exercises
    1 project | | 28 Aug 2021
    Also I would suggest is that you import a paradox (e.g., and see what it actually does when you construct values with it that you evaluate or proofs that you use.
  • Trouble with Proving Termination without K
    2 projects | | 20 Jan 2021
    Andrea had some code relaxing these restrictions at the last AIM (cf. "trying to make termination checker accept more definitions --without-K, fixing #4527" in the wrap-up section) but I don't know if it has been merged into master yet.
  • Road to 1.0/ Zig
    2 projects | | 22 Dec 2020
    Significant nit: this isn't true. The whole domain of "high-assurance software" is about this, with examples such as CompCert and seL4. There are tools like Frama-C that support you in proving things about your C; [proof assistants]() that let you extract Haskell, OCaml, or Scheme from proofs so the code is correct by construction; and languages like CakeML, F*, Agda, Idris, ATS... that are both programming languages and proof assistants.

What are some alternatives?

When comparing multiset and Agda you can also consider the following projects:

lean - Lean Theorem Prover

zig - General-purpose programming language and toolchain for maintaining robust, optimal, and reusable software.

HoleyMonoid - Automatically exported from

agda-vim - Agda interaction in vim

open-typerep - Open type representations and dynamic types

miso - :ramen: A tasty Haskell front-end framework

permutation - git import of patrick perry permutations lib from darcs

map-syntax - Syntax sugar and explicit semantics for statically defined maps

fgl - A Functional Graph Library for Haskell

distributive - Dual Traversable

eliminators - Dependently typed elimination functions using singletons

agda-mode-vscode - agda-mode on VS Code