All Projects → ice1000 → agda-mode

ice1000 / agda-mode

Licence: Apache-2.0 license
Accessing Agda's interaction mode via command line & external tactic for Agda.

Programming Languages

rust
11053 projects

Projects that are alternatives of or similar to agda-mode

agda-mode-vscode
agda-mode on VS Code
Stars: ✭ 112 (+330.77%)
Mutual labels:  agda
agda-from-nothing
A workshop on learning Agda with minimal prerequisites.
Stars: ✭ 74 (+184.62%)
Mutual labels:  agda
SymmetryBookFormalization
Univalent mathematics in Agda
Stars: ✭ 117 (+350%)
Mutual labels:  agda
dicy
A builder for LaTeX, knitr, literate Agda, literate Haskell and Pweave that automatically builds dependencies.
Stars: ✭ 22 (-15.38%)
Mutual labels:  agda
cubical-1lab
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
Stars: ✭ 93 (+257.69%)
Mutual labels:  agda
language-agda
Agda language support for the Atom editor
Stars: ✭ 13 (-50%)
Mutual labels:  agda
ConsHoTT
Constructive Interpretations of HoTT
Stars: ✭ 33 (+26.92%)
Mutual labels:  agda
TypeTopology
Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.
Stars: ✭ 132 (+407.69%)
Mutual labels:  agda
agda
The theory of algebraic graphs formalised in Agda
Stars: ✭ 67 (+157.69%)
Mutual labels:  agda
cubical-categories
Category theory formalized in cubical agda
Stars: ✭ 20 (-23.08%)
Mutual labels:  agda
cain
Category theory applied to functional programming (undergraduate project)
Stars: ✭ 27 (+3.85%)
Mutual labels:  agda
gentle-intro-to-reflection
A slow-paced introduction to reflection in Agda. ---Tactics!
Stars: ✭ 58 (+123.08%)
Mutual labels:  agda
agda-language-server
Language Server for Agda
Stars: ✭ 81 (+211.54%)
Mutual labels:  agda
msla2014
wherein I implement several substructural logics in Agda
Stars: ✭ 24 (-7.69%)
Mutual labels:  agda
universe-of-syntax
A universe of scope- and type-safe syntaxes (syntices?). Includes generic implementation of type-preserving renaming/substitution with all the proofs you could possibly need.
Stars: ✭ 16 (-38.46%)
Mutual labels:  agda
org-agda-mode
An Emacs mode for working with Agda code in an Org-mode like fashion, more or less.
Stars: ✭ 14 (-46.15%)
Mutual labels:  agda
Agda
Agda is a dependently typed programming language / interactive theorem prover.
Stars: ✭ 1,699 (+6434.62%)
Mutual labels:  agda
cat
A formalization of category theory in cubical Agda
Stars: ✭ 50 (+92.31%)
Mutual labels:  agda
frp agda
Functional Reactive Programming with Agda
Stars: ✭ 22 (-15.38%)
Mutual labels:  agda
agda-fragment
Algebraic proof discovery in Agda
Stars: ✭ 28 (+7.69%)
Mutual labels:  agda

agda-mode

Crates.io Crates.io Crates.io docs.rs Actions Status dep-svg Gitter

Binary download

Accessing Agda's interaction mode via command line. This library is created for agda-tac. It works with stable rust starting from 1.47.0.

This crate works with Agda >=2.6.1. Tracking issues for the required features: agda#4183, agda#4209 and agda#5052.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].