Verified Commit 8e116dfc authored by Tej Chajed's avatar Tej Chajed

Expand failure tests

parent 30fd168e
......@@ -2,3 +2,11 @@
: string
The command has indeed failed with message:
Uncaught Ltac2 exception: InvalidIdent ("has a space")
"test_not_string"
: string
The command has indeed failed with message:
Uncaught Ltac2 exception: NotStringLiteral (constr:(4))
"test_not_literal"
: string
The command has indeed failed with message:
Uncaught Ltac2 exception: NotStringLiteral (constr:(s))
......@@ -20,3 +20,17 @@ Proof.
Fail let x := string_to_ident "has a space" in
idtac x.
Abort.
Check "test_not_string".
Lemma test_not_string : True.
Proof.
Fail let x := string_to_ident 4 in
idtac x.
Abort.
Check "test_not_literal".
Lemma test_not_literal (s:string) : True.
Proof.
Fail let x := string_to_ident s in
idtac x.
Abort.
......@@ -7,7 +7,7 @@ From iris.proofmode Require Import ltac_tactics.
Import List.ListNotations.
Local Open Scope list.
Ltac2 Type exn ::= [ InvalidIdent(string) ].
Ltac2 Type exn ::= [ NotStringLiteral(constr) | InvalidIdent(string) ].
Module StringToIdent.
......@@ -39,6 +39,7 @@ Module StringToIdent.
match! s with
| EmptyString => 0
| String _ ?s' => Int.add 1 (coq_string_length s')
| _ => Control.throw (NotStringLiteral(s))
end.
Ltac2 compute c :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment