I simply want to create a concrete string and do stuff with it as if coq was a programming language. How do I create a string?
I tried:
(* From Coq Require Export String. *)
(* Compute "hello". *)
(* Require Import Ascii String. *)
(* Compute "hello". *)
(* Open Local Scope char_scope. *)
(* Compute "hello". *)
(* Example Space := " ". *)
Module Export StringSyntax.
End StringSyntax.
(* Example HelloWorld := " ""Hello world!"" ".
Compute "hello". *)
Print "hello".
which none work the way:
Compute 2.
displays:
= 2
: nat
How do I create an actual string or symbol so I can pass it to functions I create etc?
super hacky....but wish it was different:
Inductive my_parens : Type :=
| LeftMyParen
| RightMyParen.
Notation "<<<<" := LeftMyParen.
Notation ">>>>" := RightMyParen.
Compute LeftMyParen.
Compute RightMyParen.
out
= <<
: my_parens
= <<<<
: my_parens
= >>>>
: my_parens
You just had the scope wrong:
Require Import Coq.Strings.String.
Open Scope string_scope. (* NB *)
Compute "Hello, world!".