diff options
| author | letouzey | 2009-11-12 11:10:46 +0000 |
|---|---|---|
| committer | letouzey | 2009-11-12 11:10:46 +0000 |
| commit | f30347427516e70bb720fc7ed1a08a4f055bae9e (patch) | |
| tree | 2850d3acfa8182e06010b58c2e05881fdc51e018 /test-suite/output/NumbersSyntax.out | |
| parent | 3e5b93760241671c8959da1cdb8023cfa7f62987 (diff) | |
Repair interpretation of numeral for BigQ, add a printer (close #2160)
on the way:
- Added a testsuite output file
- Try to avoid nasty unfolding (fix nfun ...) in type of I31.
Idealy we would need a "Eval compute in" for the type of a inductive
constructor
- Stop opening Scopes for BigQ, BigN, BigZ by default
The user should do some Open Scope.
TODO: there's a bug that prevent BigQ.opp to have arg in bigQ_scope
(and so on for other operations), even with some Bind Scope around.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12504 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/NumbersSyntax.out')
| -rw-r--r-- | test-suite/output/NumbersSyntax.out | 56 |
1 files changed, 56 insertions, 0 deletions
diff --git a/test-suite/output/NumbersSyntax.out b/test-suite/output/NumbersSyntax.out new file mode 100644 index 0000000000..1a8f4eff13 --- /dev/null +++ b/test-suite/output/NumbersSyntax.out @@ -0,0 +1,56 @@ +I31 + : digits31 int31 +2 + : int31 +660865024 + : int31 +2 + 2 + : int31 +2 + 2 + : int31 + = 4 + : int31 + = 710436486 + : int31 +2 + : BigN.t_ +1000000000000000000 + : BigN.t_ +2 + 2 + : BigN.t_ +2 + 2 + : BigN.t_ + = 4 + : BigN.t_ + = 37151199385380486 + : BigN.t_ +2 + : BigZ.t_ +-1000000000000000000 + : BigZ.t_ +2 + 2 + : BigZ.t_ +2 + 2 + : BigZ.t_ + = 4 + : BigZ.t_ + = 37151199385380486 + : BigZ.t_ +2 + : BigQ.t_ +-1000000000000000000 + : BigQ.t_ +2 + 2 + : bigQ +2 + 2 + : bigQ + = 4 + : bigQ + = 37151199385380486 + : bigQ +BigQ.Qq 6562%bigZ 456%bigN + : BigQ.t_ + = BigQ.Qq 3281%bigZ 228%bigN + : bigQ + = BigQ.Qq 1%bigZ 10000%bigN + : bigQ |