Trouble with Proving Termination without K

This page summarizes the projects mentioned and recommended in the original post on reddit.com/r/agda

Our great sponsors
  • SonarQube - Static code analysis for 29 languages.
  • Scout APM - Less time debugging, more time building
  • OPS - Build and Run Open Source Unikernels
  • Agda

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

    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.

  • agda-playground

    I have the full code here, if anyone is interested.

  • SonarQube

    Static code analysis for 29 languages.. Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts