Category Archives: M1F

Rational powers

Lean’s core library has no support for rational or real numbers ­čśŽ They are however in the maths library — or we can just make some fake real numbers and use them instead. — let’s define the real numbers to … Continue reading

Posted in Learning Lean, M1F | Leave a comment

Sheet 1 Q2,Q3

I’ve solved Q2 and Q3 of M1F Sheet 1 and pushed the solutions to github. Q4 I somehow want to persuade Xena to do herself, but I don’t quite know the best way to do this. These questions were much … Continue reading

Posted in M1F | Leave a comment

First question done!

I have finally typed up full proofs for Xena, for the first question of M1F sheet 1. Here are the questions in traditional PDF format: Example Sheet 1. Here’s a link to a live Lean session containing the┬áSolutions to all … Continue reading

Posted in M1F | Leave a comment