summaryrefslogtreecommitdiff
path: root/test-suite/output/RealSyntax.v
blob: d976dcc1aa41130fcf9a3be543599ab4957844d9 (plain)
1
2
3
Require Reals.
Check ``32``.
Check ``-31``.