Agda mode not converting unicode commands to symbols
I recently installed (or at least think I have) agda and agda-mode. The problem is that when I type a symbol like "\to" or "\bV" on Emacs, they stay that way and don't convert to the desired symbol. But when I copy paste it from outside the application, they show perfectly fine. Im not sure what Im doing wrong since it seems that I have agda and agda-mode installed:
I also tried doing
Alt+X
set-input-method
Agda
But still when I write something like "\forall" it stays that way and doesn't convert to a symbol.
Im using agda 2.6.4.1 and Emacs 29.2 on Windows 10.
OK I think I found the issue. I was copy-pasting the backlash \ instead of manually inserting it because "Ctrl+Alt+' " or Alt+92 conflicts with Emacs shortcuts. And turns out that pasting the backlash instead of manually typing it doesn't trigger emacs-mode. You have to manually insert the backlash using the keyboard instead of pasting it -.-. So that was it.
- Can a dependently typed language be Turing complete?
- How to create a list of elements of an indexed data type, whose length depends on the index
- Failed to solve constraints: (k ≤ 5) x (k * 2 ≡ 5). How could I make this work?
- Inductive relations: Explicit proof that inverse relation is refl
- Agda mode not converting unicode commands to symbols
- Agda allows for incorrect proofs?
- Agda: Why does the compiler demand Set_1, not Set in a data definition?
- Agda: Could not parse the application
- Agda error: Importing module IO using the --guardedness flag from a module which does not
- Agda error: Not in scope when compiling example from documentation
- How to prove that equal function types have equal domains?
- How can I prove dependent function types equal in Agda?
- stuck on a proof (modeling IMP language)
- Agda proving Bool ≢ ⊤
- Why can some disjoint and exhaustive patterns not be represented as definitional equalities?
- Agda Recursion on Proof
- Agda Unresolved Metas
- Lexicographic ordering of pairs/lists in Agda using the standard library
- Cubical Agda Inclusion Order
- How to deal with non-termination error in Cubical Agda
- How to use agda almost without data, only with postulates?
- Agda - Counting Fixpoint In constructors
- sum of Fin maps in Agda
- Ill-typed with abstraction while pattern matching on the decideable comparator, union type and dependent pair agda
- Agda: agda unfolds the function definition excessively
- How to prove that a functional is injective in Agda?
- How to use Cabal dependencies from Agda's Haskell FFI?
- Agda how to run compiled .agdai binaries?
- How do I prove two applications of the absurd pattern result in the same in Cubical Agda?
- What axiom makes you be able to skip definition for impossible input for function in Agda?