Agda is a dependently typed functional programming language: It has inductive families, which are similar to Haskell's GADTs, but they can be indexed by values and not just types. To use Agda in editors like Emacs or Atom you need to enable/configure the editor to agda-mode.
Questions tagged [agda-mode]
37 questions
6
votes
2 answers
Agda: Can't find std-lib when installing with Stack
I'm trying to compile an Agda file, but I'm having trouble getting it to find the standard library. I've seen the documentation here.
I've used Stack to install it:
> which agda
/home/joey/.local/bin/agda
And I've set the environment variable for…
jmite
- 8,171
- 6
- 40
- 81
3
votes
0 answers
Unable to install agda via homebrew in mac os x M1 chip
I was following the instruction here and it said to do:
brew install agda
agda-mode setup
I believe it should be working since I was able to compile the hello-world.agda and run the binary executable with ./hello-world.
But the output says there…
Charlie Parker
- 5,884
- 57
- 198
- 323
3
votes
1 answer
Emacs doesn't see agda when launched from an .sh script
I made an .sh script with the following code
#!/bin/sh
cd ~/Projects/Agda\ projects/
emacs
But whenever I launch it I get the following error
File is missing: Cannot open load file, no such file or directory, /bin/bash: agda-mode: command not…
3
votes
1 answer
What are the general forms for type ascription in Agda?
Background: I'm working through Prabakhar Ragde's "Logic and Computation Intertwined", a totally fantastic introduction to computational intuitionistic logic. In his last chapter, he walks through some basics using Agda. I've successfully installed…
John Clements
- 16,895
- 3
- 37
- 52
3
votes
1 answer
Agda - Building proofs interactively - How to use the hole syntax?
Sorry for the strange title, I have no idea how these concepts are actually named.
I'm following an Agda tutorial and there's a section explaining how to build proofs inductively: https://plfa.github.io/Induction/#building-proofs-interactively
It's…
SwiftedMind
- 3,701
- 3
- 29
- 63
3
votes
2 answers
How do I type m≤n in Emacs's Agda mode without it turning into m≰?
What is the best way to type something like m≤n in Emacs's Agda mode?
If I type m \ < = n I get m≰, which is annoying.
My current workaround is to type m \ < = Space Backspace n but it is not very ergonomic.
Is there something I can do that doesn't…
hugomg
- 68,213
- 24
- 160
- 246
3
votes
1 answer
How do I check whether an agda term associated with a specific name relies on hole?
For the purpose of a script I would like to query the agda compiler about the definition of a function in an agda source file. I would like to ask the question: does the function named by X rely on a hole, or not? (i.e. is it a "completed proof", or…
ttbo
- 55
- 3
3
votes
0 answers
Some strangeness with agda-mode for Agda 2.5.1
So like other Agda enthusiasts, with the release of the new version of Agda, I quickly cabal-force-installed the latest and greatest. However, after compiling and setting-up agda-mode (the new one), my emacs is giving me some strange settings.
I no…
Musa Al-hassy
- 982
- 1
- 7
- 12
2
votes
1 answer
Agda Installation PLFA Configuration
I am trying to use the Programming Language Foundation with Agda plfa library, however the import does not appear to be working properly.
I have cloned the repository and added the repository path to: ~/.agda/libraries and plfa to…
John Fisher
- 243
- 3
- 10
2
votes
2 answers
Unable to open 'Agda': AbstractContextKeyService has been disposed
I'm trying to use agda-mode on visual studio code on windows 10. I'm getting this error on VSC when pressing ctrl-c ctrl-l (or any other) keybinding associated with agda-mode. I had this issue a couple of days ago, but restarting my computer solved…
kuco 23
- 786
- 5
- 18
2
votes
0 answers
Agda: How to check the type even when file doesn't typecheck yet?
In agda-mode there is C-c C-d command to infer a type of expression. This is especially needed when we arrive at a type error! But exactly then this command doesn't work. I would guess that this is because the feature wants to evaluate the…
zaabson
- 151
- 12
2
votes
0 answers
Inexplicable Lexical error compling Agda file
(Hello, thanks in advance)
I'm working through the introduction to HoTT in agda
https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/index.html
and Started my own Agda project (2 files, hardly a project) as I work through the lecture notes,…
Mzk Levi
- 814
- 7
- 14
2
votes
1 answer
Calling a function in Agda
I have this code which is basically a hello world, with an addition function, it compiles and runs and outputs 'Hello, world 5!':
open import Common.IO
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
-- how to call a function in agda i.e. '_+_(5,…
Adjam
- 598
- 1
- 8
- 22
2
votes
1 answer
How can I use agda2-mode to generate patterns when I expect to see an absurd pattern?
For example, we're proving 2 + 2 != 5:
data _+_≡_ : ℕ → ℕ → ℕ → Set where
znn : ∀ {n} → zero + n ≡ n
sns : ∀ {m n k} → m + n ≡ k → suc m + n ≡ suc k
And I can manually prove it:
2+2≠5 : 2 + 2 ≡ 5 → ⊥
2+2≠5 (sns (sns ()))
But I want the pattern…
ice1000
- 6,406
- 4
- 39
- 85
2
votes
0 answers
Guidance on very shallow embedding VHDL in AGDA Part II
Hi I asked a question regarding my project here I have worked on it a fair amount and have made the following progress:
module project1 where
open import Data.Empty
open import Data.Unit hiding (_≟_)
open import Data.Nat hiding (_≟_; _⊔_)
open…
danny
- 400
- 2
- 18