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

Stats:

CreatedMar 12, 2019
PublishedMar 12, 2019
Warriors Trained2008
Total Skips66
Total Code Submissions732
Total Times Completed384
Agda Completions167
Coq Completions160
Lean Completions97
Total Stars26
% of votes with a positive feedback rating90% of 83
Total "Very Satisfied" Votes70
Total "Somewhat Satisfied" Votes9
Total "Not Satisfied" Votes4
Total Rank Assessments4
Average Assessed Rank
8 kyu
Highest Assessed Rank
8 kyu
Lowest Assessed Rank
8 kyu
Ad
Contributors
  • ice1000 Avatar
  • donaldsebleung Avatar
  • solitude Avatar
Ad