string_ident.v 880 Bytes
Newer Older
Tej Chajed's avatar
Tej Chajed committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
From iris.proofmode Require Import string_ident.
From Coq Require Import Strings.String.
From stdpp Require Import base.
Open Scope string.

(* these tests should test name generation directly, which Mangle Names
interferes with *)
Unset Mangle Names.

Lemma test_basic_ident :  (n:nat), n = n.
Proof.
  let x := string_to_ident "n" in
  intros x.
  exact (eq_refl n).
Qed.

Lemma test_in_scope (n:nat) : n = n.
Proof.
  let x := string_to_ident "n" in exact (eq_refl n).
Qed.

Check "test_invalid_ident".
Lemma test_invalid_ident : True.
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.