lean2/tests/lean/626b.hlean

5 lines
89 B
Text
Raw Permalink Normal View History

import homotopy.circle
open circle
definition f (x : S¹) : bool := circle.rec_on x _ _