How does one compute/create a concrete/actual string in coq to pass to functions or store in a variable/identifier?

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

>Solution :

You just had the scope wrong:

Require Import Coq.Strings.String.
Open Scope string_scope. (* NB *)
Compute "Hello, world!".

Leave a Reply