aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/RealSyntax.v8
blob: 2e4feeef05c5e3fbca7aa0f8adbc3470b689e055 (plain)
1
2
3
Require Import Reals.
Check 32%R.
Check (-31)%R.