Stack Overflow
Stack Overflow

Questions tagged [agda-stdlib]

17 questions
2
votes
1 answer

How to shuffle a list i agda?

I would like to randomly shuffle a list in agda. I thought about taking random n elements from the beginning and adding them to the end, but I couldn't get the random part to work from this approach. Is this possible with pattern matching or do I…
weyh
  • 169
  • 2
  • 5
2
votes
1 answer

Modular arithmetic proofs in agda

I'm trying to prove (n : ℕ) → ∃[ m ] n * n ≡ 3 * m + 2 → ⊥. Typically I would prove this by rewriting it in terms of congruence, and then splitting on each case. There doesn't seem to be a modular arithmetic module in agda-stdlib. How should I…
Ace shinigami
  • 1,374
  • 2
  • 12
  • 25
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
1
vote
1 answer

lookup using Maps from Data.Tree.AVL.Map in Agda

I don't understand how to use the provided Map from Stdlib. I tried creating a Map from String to String, and it worked, but whenever I try using the lookup function I get weird errors: This is a simplification of my code: open import…
xbreu
  • 65
  • 1
  • 6
1
vote
1 answer

Need help converting number to string in Agda

New to Agda. I want a way to obtain some output from the code, so I am looking for a way to print numbers. Found a function in the standard library but I am unable to import it. I get the following: Unsolved metas at the following locations: …
gintunas
  • 13
  • 2
1
vote
1 answer

Unresolved metas in for run in Agda hello-world

I tried to compile the hello-world example with Agda 2.6.1.3 and Agda stdlib 1.5. Below is the code: module hello-world where open import IO main = run (putStrLn "Hello, World!") When compiling with Agda (agda --compile hello-world.agda), the…
Ruifeng Xie
  • 813
  • 4
  • 16
1
vote
1 answer

Agda: std-lib: List: check that a filtered list is empty

I have a function filter': filter' : {A : Set} → (A → Bool) → List A → List A filter' p [] = l.[] filter' p (x ∷ xs) with (p x) ... | true = x l.∷ filter' p xs ... | false = filter' p xs and a function…
fsuna064
  • 195
  • 1
  • 7
1
vote
0 answers

Co W in agda: cannot implement RawMonad instance due to universe levels

I'm toying with functor pairs a la https://blog.functorial.com/posts/2017-12-10-Co-Finds-A-Pairing.html and https://hackage.haskell.org/package/kan-extensions-5.2.1/docs/Control-Monad-Co.html#t:CoT I am not very practiced with universe levels,…
cspollard
  • 11
  • 2
1
vote
1 answer

Preventing development agda from breaking basic standard library usage?

I'm working with the development version of agda, which is now incompatible with the basic standard library version 1.3. wmacmil@w:~/.agda$ agda --version Agda version 2.6.2-41b6b25 A basic failure.agda file, module failure where open import…
user5775230
0
votes
0 answers

writing a dependent type in agda to guarantee a list is sorted

I have a record type, call if Foo, in Agda. I can sort it by generating a String representation (display foo) and sorting the resulting strings. I have a relation, call it <=Foo, for comparing Foo records which has one constructor, $<=Foo$, that…
mattdf
  • 11
  • 2
0
votes
1 answer

Ill-typed with abstraction while pattern matching on the decideable comparator, union type and dependent pair agda

I have an object, which is represented as a function L → A ⊎ B. I usually denote it as N. It is some mapping from label l to either A or B. I have two types of reductions (in my example reductionType1 and reductionType2) and a mapping between them,…
Ilya Kolomin
  • 23
  • 5
0
votes
0 answers

How to fix errors in "Total Parser Combinators" by Nils Anders Danielsson

Note: This was originally posted with incorrect error message and is now corrected. Am trying to compile the Agda source code associated with the paper Total Parser Combinators by Nils Anders Danielsson. The source code is available here github.…
systemcpro
  • 856
  • 1
  • 7
  • 15
0
votes
1 answer

Pointwise Equality ≗ vs Propositional Equality ≡ in Agda

When trying to prove a property over functions using list, I had to prove that the property is preserved by map over a list. Gladly, I found this useful congruence proof in Agda's standard library (here): map-cong : ∀ {f g : A → B} → f ≗ g → map f ≗…
PaulProgrammerNoob
  • 624
  • 6
  • 19
0
votes
0 answers

proof by contraposition in agda using solvers

can you use the Nat solver in agda-stdlib for proof by contradiction? In particular I have a gnarly bit of algebra I'd rather not do by hand, but I'm not sure how to use a solver to make my life easier. For reference this is the result I want to…
Ace shinigami
  • 1,374
  • 2
  • 12
  • 25
0
votes
1 answer

Termination checking failed

I was trying to train on this kata about longest common subsequences of a list which I slightly modified so that it worked with my versions of agda and the standard library (Agda 2.6.2, stdlib 1.7) which results in this code {-# OPTIONS --safe…
Junkyards
  • 25
  • 4
1
2