aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/RealSyntax.v
blob: 15ae66010e78f571d86a7dbc722b3d2b95405131 (plain)
1
2
3
Require Import Reals.
Check 32%R.
Check (-31)%R.