/tower-of-hanoi

proof using the lean prover that the towers of hanoi problem is solvable

Primary LanguageLean

tower-of-hanoi

proof that the towers of hanoi problem is solvable using the lean prover

mostly an exercise in wrangling with vectors lol. it is absolutely possible to do this way more elegantly. possibly using arrays instead of vectors.