This is a template Lean4 homework assignment using lean_grader, meant primarily for use with github classrooms.
It has two dependencies: lean_grader and mathlib4.
The lean_grader repo introduces a lake executable grade which is used for the grading procedure.
The CI in this repo should behave well with respect to github classrooms.
Just modify the hash in the file .github/classroom/autograding.json as described above.