-
Notifications
You must be signed in to change notification settings - Fork 0
/
index.html
43 lines (38 loc) · 1.37 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="content-type" content="text/html;charset=utf-8" />
<title>Using jsCoq with NPM (a template)</title>
<!-- important: this will not work from *within* the jsCoq package dir; -->
<!-- this template is meant to be copied to your project dir and edited -->
<script src="node_modules/jscoq/ui-js/jscoq-loader.js"></script>
<!-- import { JsCoq } from 'node_modules/jscoq/frontend/classic/js/index.js'; -->
</head>
<body class="jscoq-main">
<div id="ide-wrapper" class="toggled">
<div id="code-wrapper">
<div id="document">
<h1>Write a header here</h1>
<p>
Write some text as well.
</p>
<textarea id="coq-code">
Require Import UniMath.Foundations.All.
</textarea>
</div>
</div>
</div>
<!-- jsCoq configuration part -->
<script type="text/javascript">
var jscoq_ids = ['coq-code'];
var jscoq_opts = {
prelude: true,
implicit_libs: true,
base_path: './node_modules/jscoq/',
editor: { mode: { 'company-coq': true }, keyMap: 'default' },
init_pkgs: ['init'],
all_pkgs: {'+': ['coq'], 'UniMath/_build/default/coq-pkgs': ['unimath']}
};
JsCoq.start(jscoq_opts.base_path, './node_modules', jscoq_ids, jscoq_opts);
</script>
</body>