8 kyu
Theorem proving hello world: prove a+0=a and 0+a=a
167 of 384ice1000
Description:
This is a 8kyu theorem proving Kata which takes you to the world of theorem proving.
The proof is already in the standard library.
All the definitions are changeable and this Kata is easily hackable. I do this intentionally because once you know how to hack this, you should head to more complicated Katas. Hacking this 8kyu does not benefit you much.
Read Agda documentation to see how to edit Agda codes locally and how to install Agda.
Theorem Proving
Fundamentals
Similar Kata:
Stats:
Created | Mar 12, 2019 |
Published | Mar 12, 2019 |
Warriors Trained | 2008 |
Total Skips | 66 |
Total Code Submissions | 732 |
Total Times Completed | 384 |
Agda Completions | 167 |
Coq Completions | 160 |
Lean Completions | 97 |
Total Stars | 26 |
% of votes with a positive feedback rating | 90% of 83 |
Total "Very Satisfied" Votes | 70 |
Total "Somewhat Satisfied" Votes | 9 |
Total "Not Satisfied" Votes | 4 |
Total Rank Assessments | 4 |
Average Assessed Rank | 8 kyu |
Highest Assessed Rank | 8 kyu |
Lowest Assessed Rank | 8 kyu |