Do you use Idris or Coq, and why?

1. agda2hs

   1 4 188 8.8 Agda

   Compiling Agda code to readable Haskell

   

   My concrete long term strategy is to learn Agda well enough that I can write all logic exclusively in Agda and then extract Haskell through agda2hs.

2. InfluxDB

   www.influxdata.com featured

   InfluxDB – Built for High-Performance Time Series Workloads. InfluxDB 3 OSS is now GA. Transform, enrich, and act on time series data directly in the database. Automate critical tasks and eliminate the need to move data externally. Download now.

   

3. Agda

   2 27 2,640 9.9 Haskell

   Agda is a dependently typed programming language / interactive theorem prover.

   

   Funny that you say this, because there are some obvious long standing open feature requests with looking up the type of the term under cursor — № 4295 and № 516. I am not blaming anyone in particular — this is the way it is. I wish I could find time to rewrite the proof search engine (how hard can it be), but I am already buried under a pile of other commitments and a good chunk of overwhelming sadness.

4. hs-to-coq

   3 2 85 0.0 Coq

   Convert Haskell source code to Coq source code.

   

   There is even a project that converts Haskell to Coq.

Suggest a related project