Stream: Coq users

Topic: Coqtop help

kumar (Apr 07 2022 at 16:55):

I'm trying to use coqtop to create a simple definition that creates a function sum

Definition sum (a b : int) : int := a + b.

but I'm getting the following error

Coq < Definition sum (a b : int) : int := a + b.
Toplevel input, characters 22-25:
> Definition sum (a b : int) : int := a + b.
>                       ^^^
Error: The reference int was not found in the current environment.

how do I import int or equivalent Integer library for coq, Thanks!

Pierre Castéran (Apr 07 2022 at 16:59):

The simplest way is to replace intwith nat(Peano natural numbers) or Z (library ZArith, integers)

Gaëtan Gilbert (Apr 07 2022 at 17:07):

coqtop is not recommended, use vscoq, coqide or proof general instead

kumar (Apr 07 2022 at 17:15):

Thanks @Pierre Castéran for the help, I'll try that!

Thanks @Gaëtan Gilbert I use vscode so I'll try and use vscoq, do I need some config files or starter template or I can just create a example.v file and run the code?

Paolo Giarrusso (Apr 07 2022 at 18:33):

For a single file, just example.v :-)

kumar (Apr 08 2022 at 11:21):

Thanks @Paolo Giarrusso !

Last updated: Oct 13 2024 at 01:02 UTC