agda Questions
2
Solved
The Agda standard library contains some modules Relation.Binary.*.(Non)StrictLex (currently only for Product and List). We can use these modules to easily construct an instance of, for example, IsS...
Conchaconchie asked 23/6, 2014 at 8:57
7
Solved
Suppose we define a function
f : N \to N
f 0 = 0
f (s n) = f (n/2) -- this / operator is implemented as floored division.
Agda will paint f in salmon because it cannot tell if n/2 is smaller tha...
Antichlor asked 28/10, 2013 at 18:58
2
Solved
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/.lo...
Hervey asked 27/10, 2017 at 21:51
1
Solved
Agda's mixiture of records and the instance keyword give us behaviour similar to that of Haskell's typeclasses. Moreover, ignoring the instance keyword, we can have more than one instance for the s...
Retharethink asked 22/4, 2016 at 20:52
3
Solved
I am trying to learn agda. However, I got a problem. All the tutorials which I found on agda wiki are too complex for me and cover different aspects of programming. After parallel reading of 3 tuto...
Skeg asked 26/2, 2012 at 18:20
1
Solved
On page 12 of One Monad to Prove Them All, it is written that "a prominent example [of container] is the list data type. A list can be represented by the length of the list and a function mapp...
Izzard asked 22/2, 2022 at 19:33
1
Solved
I have the following two definitions that result in two different error messages.
The first definition is declined because of strict positivity and the second one because of a universe inconsistenc...
Whopper asked 15/5, 2019 at 7:15
3
Solved
One finds that Setoids are widely used in languages such as Agda, Coq, ... Indeed languages such as Lean have argued that they could help avoid "Setoid Hell". What is the reason for using...
1
Solved
Going at the root of Agda standard library, and issuing the following command:
grep -r "module _" . | wc -l
Yields the following result:
843
Whenever I encounter such anonymous modules ...
1
Solved
I have installed and been able to use Agda on my Ubuntu system via the emacs editor, and all seems good so far.
However, I am unable to install and set up the standard library for it.
Following ...
1
I read such a piece of code in plfa.
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; cong; sym)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
but _≡⟨_⟩_ is n...
Ninepins asked 20/4, 2020 at 8:5
1
Solved
I would like to automatically case over arguments using a syntax declared
besides the one given as a type constructor. For example,
postulate P : ℕ → ℕ → Set
data Silly : Set where
goo : (n : ℕ)...
1
Solved
I am currently implementing derivatives of regular data structures, in Agda,
as presented in the One-Hole Context paper by Conor McBride [5].
In implementing it straight out of the OHC paper, whic...
Champagne asked 15/4, 2020 at 16:21
1
Solved
I noticed that the Cubical standard library defines Fin as a dependent pair instead of an indexed inductive type. The reason why is that Cubical Agda does not fully support indexed inductive types:...
Kerril asked 28/1, 2020 at 2:29
1
Solved
Consider the following (invalid) Agda code
data Example : Example ex → Set where
ex : Example ex
This type can be writtien validly in Agda in the following way, making use of Agda's feature of ...
Amends asked 10/12, 2019 at 23:24
8
Solved
Is there a typed programming language where I can constrain types like the following two examples?
A Probability is a floating point number with minimum value 0.0 and maximum value 1.0.
type Pro...
Behnken asked 4/10, 2013 at 10:26
1
Solved
In the standard library of Cubical Agda, there are finite multisets whose elegant definitions I reproduce below:
{-# OPTIONS --cubical --safe #-}
open import Cubical.Foundations.Prelude
infixr 2...
Neopythagoreanism asked 29/9, 2019 at 11:0
1
I'm experimenting with Homotopy Type Theory in Agda. I use HITs to define the integers:
{-# OPTIONS --cubical --safe #-}
open import Cubical.Foundations.Prelude
open import Data.Nat using (ℕ; _+_...
Calamint asked 9/9, 2019 at 21:59
1
Solved
This is in continuation of this question, based on this answer. Using the technique explained by Saizan, and factoring my fromList-toList proof a bit to avoid the problematic recursion, I managed t...
Midwife asked 3/9, 2019 at 16:55
1
Solved
I am trying to write a proof for an equality in results of a function with a HIT domain. Because the function is defined over a HIT, the proof of equality also has to handle path cases. In those ca...
Canadianism asked 24/8, 2019 at 19:36
2
Solved
I'm having some trouble figuring out how to properly make a Map with String keys in Agda. I've got the following:
import Data.AVL.IndexedMap
Var = String
data Type where -- ...
alwaysType : Var...
Rapallo asked 5/3, 2017 at 21:9
3
I installed an Agda compiler, binarys can be from here: http://ocvs.cfv.jp/Agda/how-to-install-windows.html
... and I'm trying to make it compile a simple hello world app (I found the Agda 'Hello ...
1
Solved
I have been trying to write and verify a compiler in Agda, using Concrete Semantics (which is written for Coq Isabelle/HOL) as a reference point. I am defining compilation for the same languages us...
Legionnaire asked 22/11, 2018 at 16:22
2
Solved
I'd like to define a function with two, higher inductive typed, arguments in Cubical mode. I am using the cubical package as my "prelude" library.
I first define a quotient type for integers as a ...
Nissen asked 4/11, 2018 at 13:38
3
Solved
Suppose I have, using the cubical-demo library, the following things in scope:
i : I
p0 : x ≡ y
p1 : x' ≡ y'
q0 : x ≡ x'
q1 : y ≡ y'
How do I then construct
q' : p0 i ≡ p1 i
?
Abhorrent asked 5/11, 2018 at 8:17
1 Next >
© 2022 - 2024 — McMap. All rights reserved.