Working page

Welcome to the JsCoq Interactive Online System!

This page relies on the JsCoq technology developed by Emilio J. Gallego Arias. More information about this technology is available on github at https://github.com/ejgallego/jscoq.

Instructions:

Coq fragment are stored in text areas. You can move the cursor in the text area using the mouse and type your own commands. Type Alt-Enter (Cmd should work in Macs too) to make sure Coq execute commands up to the current location of the cursor. Type Alt-N to move forward one sentence of the Coq at a time and Alt-P to cancel the effect of the last executed sentence (you can also use Alt-Down/Up). The key F8 or the power icon toogles the goal panel.

A first example

The first coq fragment is here. This fragment shows how we can define our own function that adds all the elements in a list of numbers and then write a proof about this function.