文件列表:

CHANGELOG.md (311, 2023-12-16)
LICENSE (1527, 2023-12-16)
Setup.hs (46, 2023-12-16)
app/ (0, 2023-12-16)
app/InteractiveCli.hs (4417, 2023-12-16)
app/InteractiveTui.hs (10207, 2023-12-16)
app/InterpretUtils.hs (4848, 2023-12-16)
app/Main.hs (3749, 2023-12-16)
app/Server.hs (4354, 2023-12-16)
app/Server/ (0, 2023-12-16)
app/Server/Agent.hs (2419, 2023-12-16)
app/Tui/ (0, 2023-12-16)
app/Tui/Defaults/ (0, 2023-12-16)
app/Tui/Defaults/EditorKeymap.hs (7646, 2023-12-16)
app/Tui/Defaults/UnicodeInput.hs (2697, 2023-12-16)
app/Tui/Editor.hs (3105, 2023-12-16)
app/Tui/Interaction.hs (4697, 2023-12-16)
app/Tui/Keymap.hs (593, 2023-12-16)
app/Tui/Types.hs (1361, 2023-12-16)
app/Tui/Unicode.hs (4187, 2023-12-16)
docs/ (0, 2023-12-16)
docs/docs/ (0, 2023-12-16)
docs/docs/examples.html (12745, 2023-12-16)
docs/docs/index.html (8016, 2023-12-16)
docs/index.html (13410, 2023-12-16)
docs/overview.html (23746, 2023-12-16)
docs/sigil-style.css (856, 2023-12-16)
docs/tooling/ (0, 2023-12-16)
docs/tooling/assets/ (0, 2023-12-16)
docs/tooling/assets/screenshot-interactive.png (28175, 2023-12-16)
docs/tooling/index.html (13106, 2023-12-16)
package.yaml (2223, 2023-12-16)
src/ (0, 2023-12-16)
src/Backtrack.hs (2667, 2023-12-16)
src/Prettyprinter/ (0, 2023-12-16)
src/Prettyprinter/Render/ (0, 2023-12-16)
src/Prettyprinter/Render/Sigil.hs (2638, 2023-12-16)
... ...

# Sigil Sigil is a small experimental dependently-typed language. From a theoretical perspective, Sigil aims to implement Higher Observational Type Theory (HOTT). Future goals include extending the type system to include higher inductive types, and allowing excluded middle to compute while maintaining consistency. ## Usage Sigil must be cloned and build with the haskell [stack](https://docs.haskellstack.org/en/stable/) tool. From here, it can be installed with `stack install` then run with `sigil `, or, if you don't want to install, run directly with `stack run -- `. At the moment, only the 'interactive' mode is implemented, so for `` you'll need to substitute "interactive". This will drop you into a REPL, where the following actions are available: + Typing in a sigil expression will evaluate that expression, returning its' value and type (or an error) + `;q` will exit the REPL + `;load ` will load the specified file, expecting it to be a module. + `;import ` will import symbols into the REPLs' namespace. ## Syntax For an example of the syntax, see the [github page](https://rationalis-petra.github.io/Sigil) for this project, which has proper syntax highlighting. ## Status + The runtime can evaluate and check both expressions in a REPL and files/modules. + Inductive datatypes are defined, but (propositional) equality is not impemented for them. + Propositional equality is partially implemented: reduction is implemented for the function-type, but the symmetry reduction rule/term is not (and, as above, not implemented for inductive datatypes). ## Known Issues + The universe system is a mess in general; level checks are often outright wrong and not (yet) based in the proper theory.

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：