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!
The simplest way is to replace
nat(Peano natural numbers) or
coqtop is not recommended, use vscoq, coqide or proof general instead
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?
For a single file, just example.v :-)
Thanks @Paolo Giarrusso !
Last updated: Jan 28 2023 at 05:02 UTC