I am absolutely not an expert here, but you probably want dependent types to have more interesting examples. Hopefully my made up syntax is understandable f

I am absolutely not an expert here, but you probably want dependent types to have more interesting examples. Hopefully my made up syntax is understandable fermat x y z: Int -> Int -> Int -> c: (x^z+y^z=c^z and Int) This might only ever have an implementation if we hard code it to z=2.