python (65.2k questions)

javascript (44.3k questions)

reactjs (22.7k questions)

java (20.8k questions)

c# (17.4k questions)

html (16.3k questions)

r (13.7k questions)

android (13k questions)

Questions - coqide

Warning : “Set this option from the IDE menu instead” in coq

I'm studying the Chapter "Imp" of Software foundation. I runned the command Unset Printing Coercions. in Coq Ide, the coq Message warned me that "Set this option from the IDE menu inste...
test-img

Echo_Zero

coq

coq-tactic

coqide

Votes: 0

Answers: 1

Latest Answer

You should go under the "View" menu, and tick/untick the "Display coercions" button.
test-img

Meven Lennon-Bertrand

Concatenation of 2 lists in lambda-calculus

I have defined the type of a polymorphic list and its constructors, and now trying to write a fonction that concatenate 2 lists but my function concat does not work Definition listA A :Set := fora...
test-img

t1kumi

coq

lambda-calculus

coqide

Votes: 0

Answers: 1

Latest Answer

There are two issues with your function: first, you use a to build some listA A and not some A, so its first argument should be listA A and not A. Second, its third argument is also incorrect: in the ...
test-img

Meven Lennon-Bertrand

how to create a polymorphe couple such as "( a : type A, b : type B ) " in lambda-calculus

I am working on a project in Lambda-calculus and i am trying to code polymorphe couple with coqide but a have a problem coding the constructor that respect the type pprod Definition pprod : Set -> ...
test-img

t1kumi

coq

lambda-calculus

coqide

Votes: 0

Answers: 1

Latest Answer

The problem is that you are quantifying over Set, so the resulting product type cannot be of type Set, but of a larger type Type. So your definition should look like Definition pprod : Set -> S...
test-img

Couchy

How to activate the Coq messages in vscode/vscoq like in the CoqIde/jscoq?

I am expecting something in my messages bar but I don't see it Example script: Fixpoint add_left (n m : nat) : nat := match n with | O => m | S p => S (add_left p m) end. Lemma demo_1...
test-img

Charlie Parker

visual-studio-code

coq

coqide

vscoq

jscoq

Votes: 0

Answers: 1

Latest Answer

Seems it's printed in: It's not a bug, it's not printed in "Notices" but in "Info".
test-img

Charlie Parker

Posts

Questions

Blogs

Jobs