on 76ec3fe help sign in
4 lines 73 B history raw
1reg035b.idr:8:6:Can't convert
2 Additive -> Nat
3with
4 Fin 0