Closed JasonGross closed 9 years ago
Writing trunc_S seems unwieldy. I propose that, copying ssreflect, n.+1 mean S n in nat_scope and trunc_S n in trunc_scope. When I get a chance, I'll make a pull request to this effect if no one disagrees nor beats me to it.
trunc_S
n.+1
S n
nat_scope
trunc_S n
trunc_scope
+1
mikeshulman
commented
9 years ago
Writing
trunc_Sseems unwieldy. I propose that, copying ssreflect,n.+1meanS ninnat_scopeandtrunc_S nintrunc_scope. When I get a chance, I'll make a pull request to this effect if no one disagrees nor beats me to it.