Questions tagged [interface]
Use this tag to discuss interfaces to proof assistants, including Integrated Development Environments and Language Server Protocols. In computing, an interface is a shared boundary across which two or more separate components of a computer system exchange information. (from Wikipedia)
3
questions
1
vote
1
answer
39
views
Can Coq grab some data over HTTP and then write the data as declartions in Coq itself?
The data I'm referring to is just an easy to understand JSON format of objects / arrows and the styling information about the arrows.
For example, if an arrow is two-headed I need in Coq locally to ...
1
vote
1
answer
96
views
Agda - Help with importing Haskell function via FFI
I'm trying out Agda's Foreign Function Interface with a simple correctness proof of quicksort (which I have defined in Haskell), but I'm having trouble importing the Haskell function. I've been ...
- 13
9
votes
4
answers
384
views
What are the pros and cons of continuous checking over keychord-triggered checking?
As far as I know, the default configuration for the Lean VSCode plugin checks the code continuously, and so even when the user is in the middle of typing an expression, Lean will immediately report a ...
- 3,480