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
55 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 ...
user avatar
32 votes
8 answers
979 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 - ...
user avatar