diff --git a/.github/workflows/alpine.yml b/.github/workflows/alpine.yml index ecab993f82..fbaf84e201 100644 --- a/.github/workflows/alpine.yml +++ b/.github/workflows/alpine.yml @@ -49,6 +49,3 @@ jobs: - name: Check for duplicate files shell: alpine.sh {0} run: dev/tools/check-duplicate-files.sh - - name: 'make -j -k test-suite' - shell: alpine.sh {0} - run: 'make -j -k test-suite' diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml index 55e0036cc2..8dcc328370 100644 --- a/.github/workflows/nix-action-rocq-9.0.yml +++ b/.github/workflows/nix-action-rocq-9.0.yml @@ -7778,60 +7778,6 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "stdlib-refman-html" - stdlib-test: - needs: [] - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v31 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq - uses: cachix/cachix-action@v16 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq-community, math-comp - name: coq - - id: stepGetDerivation - name: Getting derivation for current job (stdlib-test) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.0\" --argstr job \"stdlib-test\" \\\n --dry-run 2> err > out || - (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting - derivation failed\"; exit 1; fi\n" - - id: stepCheck - name: Checking presence of CI target for current job - run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs - actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\ - ) ; then\n echo \"waiting a bit for derivations that should be in cache\"\ - \n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\ - status=fetched\" >> $GITHUB_OUTPUT\nfi\n" - - if: steps.stepCheck.outputs.status != 'fetched' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" - --argstr job "stdlib-test" stdpp: needs: - coq diff --git a/.nix/config.nix b/.nix/config.nix index c5b1894ff3..819705c944 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -223,11 +223,11 @@ with builtins; with (import {}).lib; rocq-elpi.override.version = "master"; rocq-elpi.override.elpi-version = "2.0.7"; rocq-elpi-test.override.version = "master"; - stdlib-test.job = true; }; in { "rocq-master" = { rocqPackages = common-bundles // { rocq-core.override.version = "master"; + stdlib-test.job = true; }; coqPackages = coq-common-bundles // { coq.override.version = "master"; }; }; diff --git a/test-suite/Makefile b/test-suite/Makefile index 314ca240b9..3f841e31c7 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -274,15 +274,6 @@ $(addsuffix .log,$(wildcard bugs/*.v success/*.v stm/*.v micromega/*.v modules/* } > "$(shell dirname $<)/$(shell basename $< .v).chk.log"; fi $(HIDE)$(call REPORT_TIMER,$(patsubst %.v.log,%.chk.log,$@)) -ROCQ_VERSION=$(shell rocq -print-version | cut -d+ -f1 | cut -d. -f1,2) - -output_for=`\ - if [ -e $(1).out.$(ROCQ_VERSION) ]; then\ - echo $(1).out.$(ROCQ_VERSION);\ - else\ - echo $(1).out;\ - fi` - $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) @echo "TEST $< $(call get_coq_prog_args_in_parens,"$<")" $(HIDE){ \ @@ -298,7 +289,7 @@ $(addsuffix .log,$(wildcard output/*.v)): %.v.log: %.v %.out $(PREREQUISITELOG) | grep -a -v "Skipping rcfile loading" \ | grep -a -v "^" \ > $$output; \ - diff -a -u --strip-trailing-cr $(call output_for,$*) $$output 2>&1; R=$$?; times; \ + diff -a -u --strip-trailing-cr $*.out $$output 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ echo " $<...Ok"; \ diff --git a/test-suite/output/Fixpoint.out.9.0 b/test-suite/output/Fixpoint.out.9.0 deleted file mode 100644 index 9988721052..0000000000 --- a/test-suite/output/Fixpoint.out.9.0 +++ /dev/null @@ -1,96 +0,0 @@ -fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : list B := - match l with - | nil => nil - | a :: l0 => f a :: F A B f l0 - end - : forall A B : Set, (A -> B) -> list A -> list B -let fix f (m : nat) : nat := match m with - | 0 => 0 - | S m' => f m' - end in f 0 - : nat -Ltac f id1 id2 := fix id1 2 with (id2 (n:_) (H:odd n) {struct H} : n >= 1) - = cofix inf : Inf := {| projS := inf |} - : Inf -File "./output/Fixpoint.v", line 57, characters 0-51: -Warning: Not a truly recursive fixpoint. [non-recursive,fixpoints,default] -File "./output/Fixpoint.v", line 60, characters 0-103: -Warning: Not a fully mutually defined fixpoint -(k1 depends on k2 but not conversely). -Well-foundedness check may fail unexpectedly. - [non-full-mutual,fixpoints,default] -File "./output/Fixpoint.v", line 62, characters 0-106: -Warning: Not a fully mutually defined fixpoint -(l2 and l1 are not mutually dependent). -Well-foundedness check may fail unexpectedly. - [non-full-mutual,fixpoints,default] -File "./output/Fixpoint.v", line 64, characters 0-103: -Warning: Not a fully mutually defined fixpoint -(m2 and m1 are not mutually dependent). -Well-foundedness check may fail unexpectedly. - [non-full-mutual,fixpoints,default] -File "./output/Fixpoint.v", line 72, characters 0-25: -Warning: Not a truly recursive cofixpoint. [non-recursive,fixpoints,default] -File "./output/Fixpoint.v", line 75, characters 0-48: -Warning: Not a fully mutually defined cofixpoint -(a2 and a1 are not mutually dependent). - [non-full-mutual,fixpoints,default] -File "./output/Fixpoint.v", line 91, characters 2-15: -The command has indeed failed with message: -Recursive definition of foo and bar is ill-formed. -As a mutual fixpoint: -Not enough abstractions in the definition. -The 1st recursive definition is: "?Goal". -The 2nd recursive definition is: "?Goal0". -The condition holds up to here. -File "./output/Fixpoint.v", line 96, characters 6-19: -The command has indeed failed with message: -Recursive definition of foo and bar is ill-formed. -As a mutual fixpoint decreasing on the 1st argument of foo and -1st argument of bar: -Recursive call to bar has principal argument equal to -"0" instead of -a subterm of "n". -As a mutual fixpoint decreasing on the 1st argument of foo and -2nd argument of bar: -Recursive call to bar has principal argument equal to -"0" instead of -a subterm of "n". -As a mutual fixpoint decreasing on the 2nd argument of foo and -1st argument of bar: -Recursive call to bar has principal argument equal to -"0" instead of -a subterm of "m". -As a mutual fixpoint decreasing on the 2nd argument of foo and -2nd argument of bar: -Recursive call to bar has principal argument equal to -"0" instead of a subterm of "m". -The 1st recursive definition is: -"fun n m : nat => - match n with - | 0 => bar 0 0 - | S n0 => (fun n1 : nat => ?Goal0@{n:=n1}) n0 - end". -The 2nd recursive definition is: "fun n m : nat => ?Goal". -The condition holds up to here. -The condition holds up to here. -The condition holds up to here. -The condition holds up to here. -File "./output/Fixpoint.v", line 123, characters 6-19: -The command has indeed failed with message: -Recursive definition of foo' and bar' is ill-formed. -As a mutual fixpoint decreasing on the 1st argument of foo' and -1st argument of bar': -Fixpoints on proof irrelevant inductive types should produce proof irrelevant -values. -As a mutual fixpoint decreasing on the 1st argument of foo' and -2nd argument of bar': -Recursive call to bar' has principal argument equal to -"0" instead of a subterm of "n". -The 1st recursive definition is: -"fun (n : nat) (m : Prop) => - match n with - | 0 => bar' SI 0 - | S n0 => (fun n1 : nat => ?Goal0@{n:=n1}) n0 - end". -The 2nd recursive definition is: "fun (n : STrue) (m : nat) => ?Goal". diff --git a/test-suite/output/StringSyntax.out.9.0 b/test-suite/output/StringSyntax.out.9.0 deleted file mode 100644 index 65668bd8a6..0000000000 --- a/test-suite/output/StringSyntax.out.9.0 +++ /dev/null @@ -1,1110 +0,0 @@ -byte_rect = -fun (P : byte -> Type) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") - (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") - (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") - (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") - (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) => -match b as b0 return (P b0) with -| "000" => f -| "001" => f0 -| "002" => f1 -| "003" => f2 -| "004" => f3 -| "005" => f4 -| "006" => f5 -| "007" => f6 -| "008" => f7 -| "009" => f8 -| "010" => f9 -| "011" => f10 -| "012" => f11 -| "013" => f12 -| "014" => f13 -| "015" => f14 -| "016" => f15 -| "017" => f16 -| "018" => f17 -| "019" => f18 -| "020" => f19 -| "021" => f20 -| "022" => f21 -| "023" => f22 -| "024" => f23 -| "025" => f24 -| "026" => f25 -| "027" => f26 -| "028" => f27 -| "029" => f28 -| "030" => f29 -| "031" => f30 -| " " => f31 -| "!" => f32 -| """" => f33 -| "#" => f34 -| "$" => f35 -| "%" => f36 -| "&" => f37 -| "'" => f38 -| "(" => f39 -| ")" => f40 -| "*" => f41 -| "+" => f42 -| "," => f43 -| "-" => f44 -| "." => f45 -| "/" => f46 -| "0" => f47 -| "1" => f48 -| "2" => f49 -| "3" => f50 -| "4" => f51 -| "5" => f52 -| "6" => f53 -| "7" => f54 -| "8" => f55 -| "9" => f56 -| ":" => f57 -| ";" => f58 -| "<" => f59 -| "=" => f60 -| ">" => f61 -| "?" => f62 -| "@" => f63 -| "A" => f64 -| "B" => f65 -| "C" => f66 -| "D" => f67 -| "E" => f68 -| "F" => f69 -| "G" => f70 -| "H" => f71 -| "I" => f72 -| "J" => f73 -| "K" => f74 -| "L" => f75 -| "M" => f76 -| "N" => f77 -| "O" => f78 -| "P" => f79 -| "Q" => f80 -| "R" => f81 -| "S" => f82 -| "T" => f83 -| "U" => f84 -| "V" => f85 -| "W" => f86 -| "X" => f87 -| "Y" => f88 -| "Z" => f89 -| "[" => f90 -| "\" => f91 -| "]" => f92 -| "^" => f93 -| "_" => f94 -| "`" => f95 -| "a" => f96 -| "b" => f97 -| "c" => f98 -| "d" => f99 -| "e" => f100 -| "f" => f101 -| "g" => f102 -| "h" => f103 -| "i" => f104 -| "j" => f105 -| "k" => f106 -| "l" => f107 -| "m" => f108 -| "n" => f109 -| "o" => f110 -| "p" => f111 -| "q" => f112 -| "r" => f113 -| "s" => f114 -| "t" => f115 -| "u" => f116 -| "v" => f117 -| "w" => f118 -| "x" => f119 -| "y" => f120 -| "z" => f121 -| "{" => f122 -| "|" => f123 -| "}" => f124 -| "~" => f125 -| "127" => f126 -| "128" => f127 -| "129" => f128 -| "130" => f129 -| "131" => f130 -| "132" => f131 -| "133" => f132 -| "134" => f133 -| "135" => f134 -| "136" => f135 -| "137" => f136 -| "138" => f137 -| "139" => f138 -| "140" => f139 -| "141" => f140 -| "142" => f141 -| "143" => f142 -| "144" => f143 -| "145" => f144 -| "146" => f145 -| "147" => f146 -| "148" => f147 -| "149" => f148 -| "150" => f149 -| "151" => f150 -| "152" => f151 -| "153" => f152 -| "154" => f153 -| "155" => f154 -| "156" => f155 -| "157" => f156 -| "158" => f157 -| "159" => f158 -| "160" => f159 -| "161" => f160 -| "162" => f161 -| "163" => f162 -| "164" => f163 -| "165" => f164 -| "166" => f165 -| "167" => f166 -| "168" => f167 -| "169" => f168 -| "170" => f169 -| "171" => f170 -| "172" => f171 -| "173" => f172 -| "174" => f173 -| "175" => f174 -| "176" => f175 -| "177" => f176 -| "178" => f177 -| "179" => f178 -| "180" => f179 -| "181" => f180 -| "182" => f181 -| "183" => f182 -| "184" => f183 -| "185" => f184 -| "186" => f185 -| "187" => f186 -| "188" => f187 -| "189" => f188 -| "190" => f189 -| "191" => f190 -| "192" => f191 -| "193" => f192 -| "194" => f193 -| "195" => f194 -| "196" => f195 -| "197" => f196 -| "198" => f197 -| "199" => f198 -| "200" => f199 -| "201" => f200 -| "202" => f201 -| "203" => f202 -| "204" => f203 -| "205" => f204 -| "206" => f205 -| "207" => f206 -| "208" => f207 -| "209" => f208 -| "210" => f209 -| "211" => f210 -| "212" => f211 -| "213" => f212 -| "214" => f213 -| "215" => f214 -| "216" => f215 -| "217" => f216 -| "218" => f217 -| "219" => f218 -| "220" => f219 -| "221" => f220 -| "222" => f221 -| "223" => f222 -| "224" => f223 -| "225" => f224 -| "226" => f225 -| "227" => f226 -| "228" => f227 -| "229" => f228 -| "230" => f229 -| "231" => f230 -| "232" => f231 -| "233" => f232 -| "234" => f233 -| "235" => f234 -| "236" => f235 -| "237" => f236 -| "238" => f237 -| "239" => f238 -| "240" => f239 -| "241" => f240 -| "242" => f241 -| "243" => f242 -| "244" => f243 -| "245" => f244 -| "246" => f245 -| "247" => f246 -| "248" => f247 -| "249" => f248 -| "250" => f249 -| "251" => f250 -| "252" => f251 -| "253" => f252 -| "254" => f253 -| "255" => f254 -end - : forall P : byte -> Type, - P "000" -> - P "001" -> - P "002" -> - P "003" -> - P "004" -> - P "005" -> - P "006" -> - P "007" -> - P "008" -> - P "009" -> - P "010" -> - P "011" -> - P "012" -> - P "013" -> - P "014" -> - P "015" -> - P "016" -> - P "017" -> - P "018" -> - P "019" -> - P "020" -> - P "021" -> - P "022" -> - P "023" -> - P "024" -> - P "025" -> - P "026" -> - P "027" -> - P "028" -> - P "029" -> - P "030" -> - P "031" -> - P " " -> - P "!" -> - P """" -> - P "#" -> - P "$" -> - P "%" -> - P "&" -> - P "'" -> - P "(" -> - P ")" -> - P "*" -> - P "+" -> - P "," -> - P "-" -> - P "." -> - P "/" -> - P "0" -> - P "1" -> - P "2" -> - P "3" -> - P "4" -> - P "5" -> - P "6" -> - P "7" -> - P "8" -> - P "9" -> - P ":" -> - P ";" -> - P "<" -> - P "=" -> - P ">" -> - P "?" -> - P "@" -> - P "A" -> - P "B" -> - P "C" -> - P "D" -> - P "E" -> - P "F" -> - P "G" -> - P "H" -> - P "I" -> - P "J" -> - P "K" -> - P "L" -> - P "M" -> - P "N" -> - P "O" -> - P "P" -> - P "Q" -> - P "R" -> - P "S" -> - P "T" -> - P "U" -> - P "V" -> - P "W" -> - P "X" -> - P "Y" -> - P "Z" -> - P "[" -> - P "\" -> - P "]" -> - P "^" -> - P "_" -> - P "`" -> - P "a" -> - P "b" -> - P "c" -> - P "d" -> - P "e" -> - P "f" -> - P "g" -> - P "h" -> - P "i" -> - P "j" -> - P "k" -> - P "l" -> - P "m" -> - P "n" -> - P "o" -> - P "p" -> - P "q" -> - P "r" -> - P "s" -> - P "t" -> - P "u" -> - P "v" -> - P "w" -> - P "x" -> - P "y" -> - P "z" -> - P "{" -> - P "|" -> - P "}" -> - P "~" -> - P "127" -> - P "128" -> - P "129" -> - P "130" -> - P "131" -> - P "132" -> - P "133" -> - P "134" -> - P "135" -> - P "136" -> - P "137" -> - P "138" -> - P "139" -> - P "140" -> - P "141" -> - P "142" -> - P "143" -> - P "144" -> - P "145" -> - P "146" -> - P "147" -> - P "148" -> - P "149" -> - P "150" -> - P "151" -> - P "152" -> - P "153" -> - P "154" -> - P "155" -> - P "156" -> - P "157" -> - P "158" -> - P "159" -> - P "160" -> - P "161" -> - P "162" -> - P "163" -> - P "164" -> - P "165" -> - P "166" -> - P "167" -> - P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b - -Arguments byte_rect P%function_scope f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 f34 f35 f36 f37 f38 f39 f40 f41 f42 f43 f44 f45 f46 f47 f48 f49 f50 f51 f52 f53 f54 f55 f56 f57 f58 f59 f60 f61 f62 f63 f64 f65 f66 f67 f68 f69 f70 f71 f72 f73 f74 f75 f76 f77 f78 f79 f80 f81 f82 f83 f84 f85 f86 f87 f88 f89 f90 f91 f92 f93 f94 f95 f96 f97 f98 f99 f100 f101 f102 f103 f104 f105 f106 f107 f108 f109 f110 f111 f112 f113 f114 f115 f116 f117 f118 f119 f120 f121 f122 f123 f124 f125 f126 f127 f128 f129 f130 f131 f132 f133 f134 f135 f136 f137 f138 f139 f140 f141 f142 f143 f144 f145 f146 f147 f148 f149 f150 f151 f152 f153 f154 f155 f156 f157 f158 f159 f160 f161 f162 f163 f164 f165 f166 f167 f168 f169 f170 f171 f172 f173 f174 f175 f176 f177 f178 f179 f180 f181 f182 f183 f184 f185 f186 f187 f188 f189 f190 f191 f192 f193 f194 f195 f196 f197 f198 f199 f200 f201 f202 f203 f204 f205 f206 f207 f208 - f209 f210 f211 f212 f213 f214 f215 f216 f217 f218 f219 f220 f221 f222 f223 f224 f225 f226 f227 f228 f229 f230 f231 f232 f233 f234 f235 f236 f237 f238 f239 f240 f241 f242 f243 f244 f245 f246 f247 f248 f249 f250 f251 f252 f253 f254 b%byte_scope -byte_rec = -fun P : byte -> Set => byte_rect P - : forall P : byte -> Set, - P "000" -> - P "001" -> - P "002" -> - P "003" -> - P "004" -> - P "005" -> - P "006" -> - P "007" -> - P "008" -> - P "009" -> - P "010" -> - P "011" -> - P "012" -> - P "013" -> - P "014" -> - P "015" -> - P "016" -> - P "017" -> - P "018" -> - P "019" -> - P "020" -> - P "021" -> - P "022" -> - P "023" -> - P "024" -> - P "025" -> - P "026" -> - P "027" -> - P "028" -> - P "029" -> - P "030" -> - P "031" -> - P " " -> - P "!" -> - P """" -> - P "#" -> - P "$" -> - P "%" -> - P "&" -> - P "'" -> - P "(" -> - P ")" -> - P "*" -> - P "+" -> - P "," -> - P "-" -> - P "." -> - P "/" -> - P "0" -> - P "1" -> - P "2" -> - P "3" -> - P "4" -> - P "5" -> - P "6" -> - P "7" -> - P "8" -> - P "9" -> - P ":" -> - P ";" -> - P "<" -> - P "=" -> - P ">" -> - P "?" -> - P "@" -> - P "A" -> - P "B" -> - P "C" -> - P "D" -> - P "E" -> - P "F" -> - P "G" -> - P "H" -> - P "I" -> - P "J" -> - P "K" -> - P "L" -> - P "M" -> - P "N" -> - P "O" -> - P "P" -> - P "Q" -> - P "R" -> - P "S" -> - P "T" -> - P "U" -> - P "V" -> - P "W" -> - P "X" -> - P "Y" -> - P "Z" -> - P "[" -> - P "\" -> - P "]" -> - P "^" -> - P "_" -> - P "`" -> - P "a" -> - P "b" -> - P "c" -> - P "d" -> - P "e" -> - P "f" -> - P "g" -> - P "h" -> - P "i" -> - P "j" -> - P "k" -> - P "l" -> - P "m" -> - P "n" -> - P "o" -> - P "p" -> - P "q" -> - P "r" -> - P "s" -> - P "t" -> - P "u" -> - P "v" -> - P "w" -> - P "x" -> - P "y" -> - P "z" -> - P "{" -> - P "|" -> - P "}" -> - P "~" -> - P "127" -> - P "128" -> - P "129" -> - P "130" -> - P "131" -> - P "132" -> - P "133" -> - P "134" -> - P "135" -> - P "136" -> - P "137" -> - P "138" -> - P "139" -> - P "140" -> - P "141" -> - P "142" -> - P "143" -> - P "144" -> - P "145" -> - P "146" -> - P "147" -> - P "148" -> - P "149" -> - P "150" -> - P "151" -> - P "152" -> - P "153" -> - P "154" -> - P "155" -> - P "156" -> - P "157" -> - P "158" -> - P "159" -> - P "160" -> - P "161" -> - P "162" -> - P "163" -> - P "164" -> - P "165" -> - P "166" -> - P "167" -> - P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b - -Arguments byte_rec P%function_scope f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 f34 f35 f36 f37 f38 f39 f40 f41 f42 f43 f44 f45 f46 f47 f48 f49 f50 f51 f52 f53 f54 f55 f56 f57 f58 f59 f60 f61 f62 f63 f64 f65 f66 f67 f68 f69 f70 f71 f72 f73 f74 f75 f76 f77 f78 f79 f80 f81 f82 f83 f84 f85 f86 f87 f88 f89 f90 f91 f92 f93 f94 f95 f96 f97 f98 f99 f100 f101 f102 f103 f104 f105 f106 f107 f108 f109 f110 f111 f112 f113 f114 f115 f116 f117 f118 f119 f120 f121 f122 f123 f124 f125 f126 f127 f128 f129 f130 f131 f132 f133 f134 f135 f136 f137 f138 f139 f140 f141 f142 f143 f144 f145 f146 f147 f148 f149 f150 f151 f152 f153 f154 f155 f156 f157 f158 f159 f160 f161 f162 f163 f164 f165 f166 f167 f168 f169 f170 f171 f172 f173 f174 f175 f176 f177 f178 f179 f180 f181 f182 f183 f184 f185 f186 f187 f188 f189 f190 f191 f192 f193 f194 f195 f196 f197 f198 f199 f200 f201 f202 f203 f204 f205 f206 f207 f208 - f209 f210 f211 f212 f213 f214 f215 f216 f217 f218 f219 f220 f221 f222 f223 f224 f225 f226 f227 f228 f229 f230 f231 f232 f233 f234 f235 f236 f237 f238 f239 f240 f241 f242 f243 f244 f245 f246 f247 f248 f249 f250 f251 f252 f253 f254 b%byte_scope -byte_ind = -fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") - (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") - (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") - (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") - (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) => -match b as b0 return (P b0) with -| "000" => f -| "001" => f0 -| "002" => f1 -| "003" => f2 -| "004" => f3 -| "005" => f4 -| "006" => f5 -| "007" => f6 -| "008" => f7 -| "009" => f8 -| "010" => f9 -| "011" => f10 -| "012" => f11 -| "013" => f12 -| "014" => f13 -| "015" => f14 -| "016" => f15 -| "017" => f16 -| "018" => f17 -| "019" => f18 -| "020" => f19 -| "021" => f20 -| "022" => f21 -| "023" => f22 -| "024" => f23 -| "025" => f24 -| "026" => f25 -| "027" => f26 -| "028" => f27 -| "029" => f28 -| "030" => f29 -| "031" => f30 -| " " => f31 -| "!" => f32 -| """" => f33 -| "#" => f34 -| "$" => f35 -| "%" => f36 -| "&" => f37 -| "'" => f38 -| "(" => f39 -| ")" => f40 -| "*" => f41 -| "+" => f42 -| "," => f43 -| "-" => f44 -| "." => f45 -| "/" => f46 -| "0" => f47 -| "1" => f48 -| "2" => f49 -| "3" => f50 -| "4" => f51 -| "5" => f52 -| "6" => f53 -| "7" => f54 -| "8" => f55 -| "9" => f56 -| ":" => f57 -| ";" => f58 -| "<" => f59 -| "=" => f60 -| ">" => f61 -| "?" => f62 -| "@" => f63 -| "A" => f64 -| "B" => f65 -| "C" => f66 -| "D" => f67 -| "E" => f68 -| "F" => f69 -| "G" => f70 -| "H" => f71 -| "I" => f72 -| "J" => f73 -| "K" => f74 -| "L" => f75 -| "M" => f76 -| "N" => f77 -| "O" => f78 -| "P" => f79 -| "Q" => f80 -| "R" => f81 -| "S" => f82 -| "T" => f83 -| "U" => f84 -| "V" => f85 -| "W" => f86 -| "X" => f87 -| "Y" => f88 -| "Z" => f89 -| "[" => f90 -| "\" => f91 -| "]" => f92 -| "^" => f93 -| "_" => f94 -| "`" => f95 -| "a" => f96 -| "b" => f97 -| "c" => f98 -| "d" => f99 -| "e" => f100 -| "f" => f101 -| "g" => f102 -| "h" => f103 -| "i" => f104 -| "j" => f105 -| "k" => f106 -| "l" => f107 -| "m" => f108 -| "n" => f109 -| "o" => f110 -| "p" => f111 -| "q" => f112 -| "r" => f113 -| "s" => f114 -| "t" => f115 -| "u" => f116 -| "v" => f117 -| "w" => f118 -| "x" => f119 -| "y" => f120 -| "z" => f121 -| "{" => f122 -| "|" => f123 -| "}" => f124 -| "~" => f125 -| "127" => f126 -| "128" => f127 -| "129" => f128 -| "130" => f129 -| "131" => f130 -| "132" => f131 -| "133" => f132 -| "134" => f133 -| "135" => f134 -| "136" => f135 -| "137" => f136 -| "138" => f137 -| "139" => f138 -| "140" => f139 -| "141" => f140 -| "142" => f141 -| "143" => f142 -| "144" => f143 -| "145" => f144 -| "146" => f145 -| "147" => f146 -| "148" => f147 -| "149" => f148 -| "150" => f149 -| "151" => f150 -| "152" => f151 -| "153" => f152 -| "154" => f153 -| "155" => f154 -| "156" => f155 -| "157" => f156 -| "158" => f157 -| "159" => f158 -| "160" => f159 -| "161" => f160 -| "162" => f161 -| "163" => f162 -| "164" => f163 -| "165" => f164 -| "166" => f165 -| "167" => f166 -| "168" => f167 -| "169" => f168 -| "170" => f169 -| "171" => f170 -| "172" => f171 -| "173" => f172 -| "174" => f173 -| "175" => f174 -| "176" => f175 -| "177" => f176 -| "178" => f177 -| "179" => f178 -| "180" => f179 -| "181" => f180 -| "182" => f181 -| "183" => f182 -| "184" => f183 -| "185" => f184 -| "186" => f185 -| "187" => f186 -| "188" => f187 -| "189" => f188 -| "190" => f189 -| "191" => f190 -| "192" => f191 -| "193" => f192 -| "194" => f193 -| "195" => f194 -| "196" => f195 -| "197" => f196 -| "198" => f197 -| "199" => f198 -| "200" => f199 -| "201" => f200 -| "202" => f201 -| "203" => f202 -| "204" => f203 -| "205" => f204 -| "206" => f205 -| "207" => f206 -| "208" => f207 -| "209" => f208 -| "210" => f209 -| "211" => f210 -| "212" => f211 -| "213" => f212 -| "214" => f213 -| "215" => f214 -| "216" => f215 -| "217" => f216 -| "218" => f217 -| "219" => f218 -| "220" => f219 -| "221" => f220 -| "222" => f221 -| "223" => f222 -| "224" => f223 -| "225" => f224 -| "226" => f225 -| "227" => f226 -| "228" => f227 -| "229" => f228 -| "230" => f229 -| "231" => f230 -| "232" => f231 -| "233" => f232 -| "234" => f233 -| "235" => f234 -| "236" => f235 -| "237" => f236 -| "238" => f237 -| "239" => f238 -| "240" => f239 -| "241" => f240 -| "242" => f241 -| "243" => f242 -| "244" => f243 -| "245" => f244 -| "246" => f245 -| "247" => f246 -| "248" => f247 -| "249" => f248 -| "250" => f249 -| "251" => f250 -| "252" => f251 -| "253" => f252 -| "254" => f253 -| "255" => f254 -end - : forall P : byte -> Prop, - P "000" -> - P "001" -> - P "002" -> - P "003" -> - P "004" -> - P "005" -> - P "006" -> - P "007" -> - P "008" -> - P "009" -> - P "010" -> - P "011" -> - P "012" -> - P "013" -> - P "014" -> - P "015" -> - P "016" -> - P "017" -> - P "018" -> - P "019" -> - P "020" -> - P "021" -> - P "022" -> - P "023" -> - P "024" -> - P "025" -> - P "026" -> - P "027" -> - P "028" -> - P "029" -> - P "030" -> - P "031" -> - P " " -> - P "!" -> - P """" -> - P "#" -> - P "$" -> - P "%" -> - P "&" -> - P "'" -> - P "(" -> - P ")" -> - P "*" -> - P "+" -> - P "," -> - P "-" -> - P "." -> - P "/" -> - P "0" -> - P "1" -> - P "2" -> - P "3" -> - P "4" -> - P "5" -> - P "6" -> - P "7" -> - P "8" -> - P "9" -> - P ":" -> - P ";" -> - P "<" -> - P "=" -> - P ">" -> - P "?" -> - P "@" -> - P "A" -> - P "B" -> - P "C" -> - P "D" -> - P "E" -> - P "F" -> - P "G" -> - P "H" -> - P "I" -> - P "J" -> - P "K" -> - P "L" -> - P "M" -> - P "N" -> - P "O" -> - P "P" -> - P "Q" -> - P "R" -> - P "S" -> - P "T" -> - P "U" -> - P "V" -> - P "W" -> - P "X" -> - P "Y" -> - P "Z" -> - P "[" -> - P "\" -> - P "]" -> - P "^" -> - P "_" -> - P "`" -> - P "a" -> - P "b" -> - P "c" -> - P "d" -> - P "e" -> - P "f" -> - P "g" -> - P "h" -> - P "i" -> - P "j" -> - P "k" -> - P "l" -> - P "m" -> - P "n" -> - P "o" -> - P "p" -> - P "q" -> - P "r" -> - P "s" -> - P "t" -> - P "u" -> - P "v" -> - P "w" -> - P "x" -> - P "y" -> - P "z" -> - P "{" -> - P "|" -> - P "}" -> - P "~" -> - P "127" -> - P "128" -> - P "129" -> - P "130" -> - P "131" -> - P "132" -> - P "133" -> - P "134" -> - P "135" -> - P "136" -> - P "137" -> - P "138" -> - P "139" -> - P "140" -> - P "141" -> - P "142" -> - P "143" -> - P "144" -> - P "145" -> - P "146" -> - P "147" -> - P "148" -> - P "149" -> - P "150" -> - P "151" -> - P "152" -> - P "153" -> - P "154" -> - P "155" -> - P "156" -> - P "157" -> - P "158" -> - P "159" -> - P "160" -> - P "161" -> - P "162" -> - P "163" -> - P "164" -> - P "165" -> - P "166" -> - P "167" -> - P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b - -Arguments byte_ind P%function_scope f f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 f34 f35 f36 f37 f38 f39 f40 f41 f42 f43 f44 f45 f46 f47 f48 f49 f50 f51 f52 f53 f54 f55 f56 f57 f58 f59 f60 f61 f62 f63 f64 f65 f66 f67 f68 f69 f70 f71 f72 f73 f74 f75 f76 f77 f78 f79 f80 f81 f82 f83 f84 f85 f86 f87 f88 f89 f90 f91 f92 f93 f94 f95 f96 f97 f98 f99 f100 f101 f102 f103 f104 f105 f106 f107 f108 f109 f110 f111 f112 f113 f114 f115 f116 f117 f118 f119 f120 f121 f122 f123 f124 f125 f126 f127 f128 f129 f130 f131 f132 f133 f134 f135 f136 f137 f138 f139 f140 f141 f142 f143 f144 f145 f146 f147 f148 f149 f150 f151 f152 f153 f154 f155 f156 f157 f158 f159 f160 f161 f162 f163 f164 f165 f166 f167 f168 f169 f170 f171 f172 f173 f174 f175 f176 f177 f178 f179 f180 f181 f182 f183 f184 f185 f186 f187 f188 f189 f190 f191 f192 f193 f194 f195 f196 f197 f198 f199 f200 f201 f202 f203 f204 f205 f206 f207 f208 - f209 f210 f211 f212 f213 f214 f215 f216 f217 f218 f219 f220 f221 f222 f223 f224 f225 f226 f227 f228 f229 f230 f231 f232 f233 f234 f235 f236 f237 f238 f239 f240 f241 f242 f243 f244 f245 f246 f247 f248 f249 f250 f251 f252 f253 f254 b%byte_scope -"000" - : byte -"a" - : byte -"127" - : byte -File "./output/StringSyntax.v", line 18, characters 11-16: -The command has indeed failed with message: -Expects a single character or a three-digit ASCII code. -"000" - : ascii -"a" - : ascii -"127" - : ascii -File "./output/StringSyntax.v", line 25, characters 11-16: -The command has indeed failed with message: -Expects a single character or a three-digit ASCII code. -"000" - : string -"a" - : string -"127" - : string -"€" - : string -"" - : string - = "a"%char - : ascii - = "a"%byte - : byte - = "a"%string - : string - = ["a"%byte] - : list byte - = ["000"; "001"; "002"; "003"; "004"; "005"; "006"; "007"; "008"; "009"; "010"; "011"; "012"; "013"; "014"; "015"; "016"; "017"; "018"; "019"; "020"; "021"; "022"; "023"; "024"; "025"; "026"; "027"; "028"; "029"; "030"; "031"; " "; "!"; """"; "#"; "$"; "%"; "&"; "'"; "("; ")"; "*"; "+"; ","; "-"; "."; "/"; "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"; ":"; ";"; "<"; "="; ">"; "?"; "@"; "A"; "B"; "C"; "D"; "E"; "F"; "G"; "H"; "I"; "J"; "K"; "L"; "M"; "N"; "O"; "P"; "Q"; "R"; "S"; "T"; "U"; "V"; "W"; "X"; "Y"; "Z"; "["; "\"; "]"; "^"; "_"; "`"; "a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; "s"; "t"; "u"; "v"; "w"; "x"; "y"; "z"; "{"; "|"; "}"; "~"; "127"; "128"; "129"; "130"; "131"; "132"; "133"; "134"; "135"; "136"; "137"; "138"; "139"; "140"; "141"; "142"; "143"; "144"; "145"; "146"; "147"; "148"; "149"; "150"; "151"; "152"; "153"; "154"; "155"; "156"; "157"; "158"; "159"; "160"; "161"; "162"; "163"; "164"; "165"; "166"; "167"; - "168"; "169"; "170"; "171"; "172"; "173"; "174"; "175"; "176"; "177"; "178"; "179"; "180"; "181"; "182"; "183"; "184"; "185"; "186"; "187"; "188"; "189"; "190"; "191"; "192"; "193"; "194"; "195"; "196"; "197"; "198"; "199"; "200"; "201"; "202"; "203"; "204"; "205"; "206"; "207"; "208"; "209"; "210"; "211"; "212"; "213"; "214"; "215"; "216"; "217"; "218"; "219"; "220"; "221"; "222"; "223"; "224"; "225"; "226"; "227"; "228"; "229"; "230"; "231"; "232"; "233"; "234"; "235"; "236"; "237"; "238"; "239"; "240"; "241"; "242"; "243"; "244"; "245"; "246"; "247"; "248"; "249"; "250"; "251"; "252"; "253"; "254"; "255"] - : list byte - = ["000"; "001"; "002"; "003"; "004"; "005"; "006"; "007"; "008"; "009"; "010"; "011"; "012"; "013"; "014"; "015"; "016"; "017"; "018"; "019"; "020"; "021"; "022"; "023"; "024"; "025"; "026"; "027"; "028"; "029"; "030"; "031"; " "; "!"; """"; "#"; "$"; "%"; "&"; "'"; "("; ")"; "*"; "+"; ","; "-"; "."; "/"; "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"; ":"; ";"; "<"; "="; ">"; "?"; "@"; "A"; "B"; "C"; "D"; "E"; "F"; "G"; "H"; "I"; "J"; "K"; "L"; "M"; "N"; "O"; "P"; "Q"; "R"; "S"; "T"; "U"; "V"; "W"; "X"; "Y"; "Z"; "["; "\"; "]"; "^"; "_"; "`"; "a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; "s"; "t"; "u"; "v"; "w"; "x"; "y"; "z"; "{"; "|"; "}"; "~"; "127"; "128"; "129"; "130"; "131"; "132"; "133"; "134"; "135"; "136"; "137"; "138"; "139"; "140"; "141"; "142"; "143"; "144"; "145"; "146"; "147"; "148"; "149"; "150"; "151"; "152"; "153"; "154"; "155"; "156"; "157"; "158"; "159"; "160"; "161"; "162"; "163"; "164"; "165"; "166"; "167"; - "168"; "169"; "170"; "171"; "172"; "173"; "174"; "175"; "176"; "177"; "178"; "179"; "180"; "181"; "182"; "183"; "184"; "185"; "186"; "187"; "188"; "189"; "190"; "191"; "192"; "193"; "194"; "195"; "196"; "197"; "198"; "199"; "200"; "201"; "202"; "203"; "204"; "205"; "206"; "207"; "208"; "209"; "210"; "211"; "212"; "213"; "214"; "215"; "216"; "217"; "218"; "219"; "220"; "221"; "222"; "223"; "224"; "225"; "226"; "227"; "228"; "229"; "230"; "231"; "232"; "233"; "234"; "235"; "236"; "237"; "238"; "239"; "240"; "241"; "242"; "243"; "244"; "245"; "246"; "247"; "248"; "249"; "250"; "251"; "252"; "253"; "254"; "255"] - : list ascii -"abc" - : string -"000" - : nat -"001" - : nat -"002" - : nat -"255" - : nat -File "./output/StringSyntax.v", line 95, characters 11-16: -The command has indeed failed with message: -Expects a single character or a three-digit ASCII code. -"abc" - : string2 -"abc" : string2 - : string2 -"abc" : string1 - : string1 diff --git a/test-suite/output/bug_19702.out.9.0 b/test-suite/output/bug_19702.out.9.0 deleted file mode 100644 index f2fc675f8f..0000000000 --- a/test-suite/output/bug_19702.out.9.0 +++ /dev/null @@ -1,21 +0,0 @@ -f1 : ∀ {n1 : nat} (n2 : nat), T n2 → T n1 - -f1 is not universe polymorphic -Arguments f1 {n1}%nat_scope n2%nat_scope w -f1 is transparent -Expands to: Constant bug_19702.f1 -Declared in library bug_19702, line 6, characters 11-13 -f1 : ∀ {n1 : nat} [n2 : nat], T n2 → T n1 - -f1 is not universe polymorphic -Arguments f1 {n1}%nat_scope [n2]%nat_scope w -f1 is transparent -Expands to: Constant bug_19702.f1 -Declared in library bug_19702, line 6, characters 11-13 -f1 : ∀ {n1 n2 : nat}, T n2 → T n1 - -f1 is not universe polymorphic -Arguments f1 {n1 n2}%nat_scope w -f1 is transparent -Expands to: Constant bug_19702.f1 -Declared in library bug_19702, line 6, characters 11-13