Trouble with Proving Termination without K

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

Our great sponsors
  • Revelo Payroll - Free Global Payroll designed for tech teams
  • Onboard AI - Learn any GitHub repo in 59 seconds
  • SonarQube - Static code analysis for 29 languages.
  • InfluxDB - Collect and Analyze Billions of Data Points in Real Time
  • 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.

  • Revelo Payroll

    Free Global Payroll designed for tech teams. Building a great tech team takes more than a paycheck. Zero payroll costs, get AI-driven insights to retain best talent, and delight them with amazing local benefits. 100% free and compliant.

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