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)

Filter by
Sorted by
Tagged with
1 vote
1 answer

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 ...
D Left Adjoint to U's user avatar
1 vote
1 answer

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 ...
Caleb Kisby's user avatar
9 votes
4 answers

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 ...
Trebor's user avatar
  • 3,480