Questions tagged [ide]

Interactive Development Environment (IDE). These are software applications used for writing and developing with programming languages and other structured grammars.

Filter by
Sorted by
Tagged with
0 votes
0 answers

How to import unimath for coq

I want to be able to import the category theory module from unimath. I already have the coqide and vscode with the coq extensions, I also have wsl. I tried downloading the library from git and used &...
noCrayCray's user avatar
5 votes
1 answer

Is there an easy-to-learn GUI of proof assistants for teenagers in maths education?

I'm a high school sophomore and I have been interested in Interactive Theorem Proving for a year or two. I found it extremely hard for my peers (lack of knowledge in mathematical logic, type theories ...
Chesium's user avatar
  • 51
6 votes
0 answers

In VSCoq, how to issue an arbitrary Gallina query via the prompt?

I’m currently trying out Visual Studio + VSCoq, having previously used Emacs + Proof General for Coq, and there’s one part of my usual workflow that I haven’t managed to replicate yet. Is there a way ...
Peter LeFanu Lumsdaine's user avatar
5 votes
1 answer

How to evaluate proof terms through opaque definitions?

Is there is a way to force computation over opaque terms, for the purposes of debugging/meta-analysis of proof scripts. I understand why Coq doesn’t do this by default, and guess it would probably ...
Kiran Gopinathan's user avatar
53 votes
10 answers

Proof assistants for beginners - a comparison

What is a good starting point to learn about proof assistants? The answer will invariably depend on the area of interest: mathematics (and its areas, e.g. algebra,combinatorics, analysis, logic), CS - ...
Piotr Migdal's user avatar