Follow

Keep Up to Date with the Most Important News

By pressing the Subscribe button, you confirm that you have read and are agreeing to our Privacy Policy and Terms of Use
Contact

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:

MEDevel.com: Open-source for Healthcare and Education

Collecting and validating open-source software for healthcare, education, enterprise, development, medical imaging, medical records, and digital pathology.

Visit Medevel

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!".
Add a comment

Leave a Reply

Keep Up to Date with the Most Important News

By pressing the Subscribe button, you confirm that you have read and are agreeing to our Privacy Policy and Terms of Use

Discover more from Dev solutions

Subscribe now to keep reading and get access to the full archive.

Continue reading