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
5 votes
1 answer
119 views

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
84 views

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
117 views

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
37 votes
8 answers
2k views

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