From b6214bd4d5d3003e9b60411a717e84277feead24 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 3 Sep 2020 13:27:00 +0200 Subject: [string notation] Handle parameterized inductives and non inductives --- test-suite/output/StringSyntax.out | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) (limited to 'test-suite/output/StringSyntax.out') diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out index e9cf4282dc..125c1bc927 100644 --- a/test-suite/output/StringSyntax.out +++ b/test-suite/output/StringSyntax.out @@ -1051,7 +1051,7 @@ Arguments byte_ind _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ "127" : byte The command has indeed failed with message: -Expects a single character or a three-digits ascii code. +Expects a single character or a three-digit ASCII code. "000" : ascii "a" @@ -1059,7 +1059,7 @@ Expects a single character or a three-digits ascii code. "127" : ascii The command has indeed failed with message: -Expects a single character or a three-digits ascii code. +Expects a single character or a three-digit ASCII code. "000" : string "a" @@ -1084,3 +1084,15 @@ Expects a single character or a three-digits ascii code. = ["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 +The command has indeed failed with message: +Expects a single character or a three-digit ASCII code. -- cgit v1.2.3 From da7787ff4f1b5192b5465ca17ece64f5ebd4f72a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 20 Oct 2020 19:07:22 +0200 Subject: Allow multiple primitive notation on the same scope and triggers Until now, declaring a number or string notation on some trigger removed all previous notations on the same scope. Bug discovered by Jason Gross while reviewing #12218. --- test-suite/output/StringSyntax.out | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'test-suite/output/StringSyntax.out') diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out index 125c1bc927..68ee7cfeb5 100644 --- a/test-suite/output/StringSyntax.out +++ b/test-suite/output/StringSyntax.out @@ -1096,3 +1096,9 @@ Expects a single character or a three-digit ASCII code. : nat 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 -- cgit v1.2.3