Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add link to Coq Platform Docs #615

Merged
merged 3 commits into from
Sep 2, 2024
Merged

Add link to Coq Platform Docs #615

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
82fdb90
Add link to Coq Platform Docs
thomas-lamiaux Sep 2, 2024
eb5cc98
Update README.md
thomas-lamiaux Sep 2, 2024
56b6675
Update README.md
thomas-lamiaux Sep 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,16 +33,18 @@ definitions are axiom-free.
- [Installation](#installation)
- [HoTT Variant](#hott-variant)

## Live demo
## Learning Equations

Try it now in your browser with [JSCoq](http://mattam82.github.io/Coq-Equations/assets/jsexamples/equations_intro.html)!
- You can discover and learn Equations through [interactive tutorials](https://coq.inria.fr/platform-docs/)
directly in your browser, or locally with Equations installed.

## Documentation

- The [reference manual](http://github.com/mattam82/Coq-Equations/raw/main/doc/equations.pdf)
provides an introduction and a summary of the commands and options.
This introduction can also be followed interactively with Equations installed:
provides a summary of the commands and options, and a brief introduction.
This introduction can also be followed interactively with Equations installed,
[equations_intro.v](http://github.com/mattam82/Coq-Equations/raw/main/doc/equations_intro.v)
or [interactively in your browser](http://mattam82.github.io/Coq-Equations/assets/jsexamples/equations_intro.html).

- A gallery of [examples](http://mattam82.github.io/Coq-Equations/examples) provides more consequent
developments using Equations.
Expand Down Expand Up @@ -150,4 +152,4 @@ install `coq-hott` and then use:
This will compile the `HoTT` library variant in addition to the standard one.
Then, after `make install`, one can import the plugin in Coq, using:

From Equations Require Import HoTT.All.
From Equations Require Import HoTT.All.