Search code examples
coq

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!".