-
Notifications
You must be signed in to change notification settings - Fork 17
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
12a5e49
commit 616c846
Showing
82 changed files
with
9,346 additions
and
8 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,64 @@ | ||
| <!DOCTYPE html><html lang="en"> | ||
|
|
||
| <head> | ||
| <meta charset="utf-8"> | ||
| <title>Data.Fin.Interpolation</title> | ||
| <link rel="stylesheet" type="text/css" id="preferredStyle" href="../default.css"> | ||
| <script> | ||
| /* Updates the stylesheet to use the preferred one. | ||
| Note that we set the link to root ++ sourceLoc because the config | ||
| is shared across the whole website, so the root may differ from | ||
| page to page. | ||
| */ | ||
| function setStyleSource (sourceLoc) { | ||
| document.getElementById("preferredStyle").href = "../" + sourceLoc + ".css"; | ||
| document.getElementById("selectPreferredStyle").value = sourceLoc; | ||
| } | ||
| /* Initialises the preferred style sheet: | ||
| 1. if there is a stored value then use that | ||
| otherwise select the default | ||
| 2. set both the css link href & the drop down menu selected option | ||
| */ | ||
| function initStyleSource () { | ||
| var preferredStyle = localStorage.getItem("stylefile"); | ||
| if (preferredStyle !== null) { | ||
| setStyleSource(preferredStyle); | ||
| } else { | ||
| setStyleSource("default"); | ||
| }; | ||
| } | ||
| function saveStyleSource (preferredStyle) { | ||
| localStorage.stylefile = preferredStyle; | ||
| } | ||
| </script> | ||
| </head> | ||
|
|
||
| <body class="namespace"> | ||
| <header> | ||
| <strong>Idris2Doc</strong> : Data.Fin.Interpolation | ||
| <nav><a href="../index.html">Index</a> | ||
|
|
||
| <select id="selectPreferredStyle"> | ||
| <option value="default">Default</option> | ||
| <option value="alternative">Alternative</option> | ||
| <option value="blackandwhite">Black & White</option> | ||
|
|
||
| </select> | ||
| </nav> | ||
|
|
||
| <script> | ||
| /* We start by initialising the style source */ | ||
| initStyleSource(); | ||
|
|
||
| /* This listens for changes on the drop down menu and updates the | ||
| css used for the current page when a selection is made. | ||
| */ | ||
| document.getElementById("selectPreferredStyle").addEventListener("change", function(){ | ||
| var selected = this.options[this.selectedIndex].value; /* the option chosen */ | ||
| setStyleSource (selected); | ||
| saveStyleSource (selected); | ||
| }); | ||
| </script> | ||
|
|
||
| </header> | ||
| <div class="container"><div id="module-header"><h1>Data.Fin.Interpolation</h1><span style="float:right">(<a href="Data.Fin.Interpolation.src.html">source</a>)</span><pre></pre></div><code></code><h2>Definitions</h2><dl class="decls"><dt id="Data.Fin.Interpolation.FromShow"><code><a class="type" href="Data.Fin.Interpolation.html#Data.Fin.Interpolation.FromShow"><span class="name function">FromShow</span></a> : <span class="type resolved" title="Prelude.Interpolation.Interpolation"><span class="name type">Interpolation</span></span> (<span class="type resolved" title="Data.Fin.Fin"><span class="name type">Fin</span></span> <span class="boundvar">n</span>)</code></dt><dd> <b>Totality</b>: <span class="keyword">total</span><br> <b>Visibility</b>: <span class="keyword">export</span></dd></dl></div><footer>Produced by Idris 2 version 0.7.0-0e83d6c7c</footer></body></html> |
133 changes: 133 additions & 0 deletions
133
docs/fin-lizzie/docs/docs/Data.Fin.Interpolation.src.html
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,133 @@ | ||
| <!DOCTYPE html><html lang="en"> | ||
|
|
||
| <head> | ||
| <meta charset="utf-8"> | ||
| <style> | ||
| .IdrisData { | ||
| color: darkred | ||
| } | ||
| .IdrisType { | ||
| color: blue | ||
| } | ||
| .IdrisBound { | ||
| color: black | ||
| } | ||
| .IdrisFunction { | ||
| color: darkgreen | ||
| } | ||
| .IdrisKeyword { | ||
| text-decoration: underline; | ||
| } | ||
| .IdrisComment { | ||
| color: #b22222 | ||
| } | ||
| .IdrisNamespace { | ||
| font-style: italic; | ||
| color: black | ||
| } | ||
| .IdrisPostulate { | ||
| font-weight: bold; | ||
| color: red | ||
| } | ||
| .IdrisModule { | ||
| font-style: italic; | ||
| color: black | ||
| } | ||
|
|
||
| .IdrisLineNumber { | ||
| text-decoration: none; | ||
| color: lightgrey; | ||
| user-select: none; | ||
| } | ||
| .IdrisLineNumber:hover { | ||
| color: darkgray; | ||
| } | ||
| .IdrisLineNumber:target { | ||
| color: gray; | ||
| } | ||
| .IdrisHighlight { | ||
| background-color: yellow; | ||
| } | ||
| </style> | ||
| <script> | ||
| function initialize() { | ||
| function handleHash(ev) { | ||
| if (!location.hash) return | ||
| let m = location.hash.match(/#(line\d+)(?:-(line\d+))?/) | ||
| if (m) { | ||
| let start = document.getElementById(m[1]) | ||
| let end = document.getElementById(m[2]) | ||
| if (start) { | ||
| if (end && end.compareDocumentPosition(start) === 4) { | ||
| ([start, end] = [end, start]) | ||
| } | ||
| // Only on page load | ||
| if (!ev) start.scrollIntoView() | ||
| let parent = start.parentElement | ||
| let lines = parent.children | ||
| let className = '' | ||
| for (let n = 0; n < lines.length; n++) { | ||
| let el = lines[n] | ||
| if (el === start) className = 'IdrisHighlight' | ||
| el.className = className | ||
| if (el === end || className && !end) className = '' | ||
| } | ||
| } | ||
| } | ||
| } | ||
| let startLine | ||
| let endLine | ||
| function handlePointerMove(ev) { | ||
| if (startLine) { | ||
| for (let el = document.elementFromPoint(ev.clientX, ev.clientY); el; el = el.parentElement) { | ||
| if (el.parentElement === startLine.parentElement) { | ||
| if (endLine !== el) { | ||
| endLine = el | ||
| update() | ||
| } | ||
| break | ||
| } | ||
| } | ||
| } | ||
| } | ||
| function update(ev) { | ||
| window.location.hash = startLine === endLine ? startLine.id : startLine.id + '-' + endLine.id | ||
| } | ||
| function handlePointerDown(ev) { | ||
| let target = ev.target | ||
| if (target.className === 'IdrisLineNumber') { | ||
| startLine = endLine = target.parentElement | ||
| window.addEventListener('pointermove', handlePointerMove) | ||
| update() | ||
| ev.preventDefault() | ||
| } | ||
| } | ||
| function handlePointerUp(ev) { | ||
| if (startLine) { | ||
| update() | ||
| window.removeEventListener('pointermove', handlePointerMove) | ||
| startLine = endLine = null | ||
| } | ||
| } | ||
| window.addEventListener('hashchange', handleHash) | ||
| window.addEventListener('pointerdown', handlePointerDown) | ||
| window.addEventListener('pointerup', handlePointerUp) | ||
| handleHash() | ||
| } | ||
| </script> | ||
| </head> | ||
| <body onload="initialize()"> | ||
| <code class="IdrisCode"> | ||
| <div id="line0"><a href="#line0" class="IdrisLineNumber"> 0 | </a><span class="IdrisKeyword">module</span> <span class="IdrisModule">Data.Fin.Interpolation</span></div> | ||
| <div id="line1"><a href="#line1" class="IdrisLineNumber"> 1 | </a></div> | ||
| <div id="line2"><a href="#line2" class="IdrisLineNumber"> 2 | </a><span class="IdrisKeyword">import</span> <span class="IdrisModule">Data.Fin</span></div> | ||
| <div id="line3"><a href="#line3" class="IdrisLineNumber"> 3 | </a></div> | ||
| <div id="line4"><a href="#line4" class="IdrisLineNumber"> 4 | </a><span class="IdrisKeyword">%default</span> <span class="IdrisKeyword">total</span></div> | ||
| <div id="line5"><a href="#line5" class="IdrisLineNumber"> 5 | </a></div> | ||
| <div id="line6"><a href="#line6" class="IdrisLineNumber"> 6 | </a><span class="IdrisKeyword">export</span> <span class="IdrisKeyword">%defaulthint</span></div> | ||
| <div id="line7"><a href="#line7" class="IdrisLineNumber"> 7 | </a><span class="IdrisFunction">FromShow</span> <span class="IdrisKeyword">:</span> <span class="IdrisType">Interpolation</span> <span class="IdrisKeyword">(</span><span class="IdrisType">Fin</span> <span class="IdrisBound">n</span><span class="IdrisKeyword">)</span></div> | ||
| <div id="line8"><a href="#line8" class="IdrisLineNumber"> 8 | </a><span class="IdrisFunction">FromShow</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">I</span> <span class="IdrisKeyword">where</span> <span class="IdrisKeyword">[</span><span class="IdrisFunction">I</span><span class="IdrisKeyword">]</span> <span class="IdrisType">Interpolation</span> <span class="IdrisKeyword">(</span><span class="IdrisType">Fin</span> <span class="IdrisBound">n</span><span class="IdrisKeyword">)</span> <span class="IdrisKeyword">where</span> <span class="IdrisFunction">interpolate</span> <span class="IdrisKeyword">=</span> <span class="IdrisFunction">show</span></div> | ||
| <div id="line9"><a href="#line9" class="IdrisLineNumber"> 9 | </a></div> | ||
| </code> | ||
| </body> | ||
| </html> |
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Large diffs are not rendered by default.
Oops, something went wrong.
Oops, something went wrong.