798 questions
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
0
votes
0
answers
53
views
Mutually recursive stack-safe functions with different types
I want to make my mutually recursive functions stack-safe, but because they have different signatures - one traverses a list and other a tree(?) of sorts - I'm not clear how to go about this.
Here's ...
-4
votes
1
answer
201
views
Tuple constructor without using a comma
I want to create a tuple by applying an expression to a fixed number
of values, and I'm not allowed to use a comma. (Question originally said colon, but that was a mistake).
For example, if f = lambda ...
joel's user avatar
- 8,132
0
votes
1
answer
36
views
j is not accessible in this context in the "parity" example
I was trying an idris2's example.
import Data.Nat
data Parity : Nat -> Type where
Even : Parity (n + n)
Odd : Parity (S (n + n))
helpEven : (j : Nat) -> Parity (S j + S j) -> ...
0
votes
0
answers
31
views
How can I regroup list concatenations in an idris type?
In Idris2 I have a predicate P : List A -> Type (It is actually a typing judgement where the list is a context, but I'm keeping the question general to avoid explaining everything). I also have a ...
1
vote
0
answers
34
views
Constructed (0 = 1) in Idris 1.3.3?
While experimenting using Idris 1.3.3, I found that the following code file typechecks:
doubleCong: {f: Nat -> Nat -> Nat} -> (prf1: (a1 = a2)) -> (prf2: (b1 = b3)) -> (f a1 b1 = f a2 ...
1
vote
0
answers
31
views
Prove that functor simplification is isomorphism
I know how to prove isomorphisms like between binary trees and rose trees, and there are also clear isomorphisms between functor transformers (Sum, Product, etc.) and simplifications, for example the ...
1
vote
1
answer
29
views
How to specify the interface from which an object comes from in idris
Say I have the following interface in idris:
interface I a b where
x : a
y : b
And then I try to define the following function:
x' : I a b => a
x' = x
But then I get this error:
Error: While ...
0
votes
0
answers
57
views
Dependent pair recursion under lambda
I'm trying to write code where I transform a curried representation of a function to a function taking a Vect argument. With the function structures I've tried, I got stuck, because I'd need to know ...
1
vote
0
answers
89
views
Why is `Prelude.mod` a total function?
Why is Prelude.mod marked as a total function when it is not defined when the second argument is zero?
Main> :total mod
Prelude.Num.mod is total
I was just bit by this and ran into a run-time ...
0
votes
1
answer
78
views
Obtaining a value that was supposed to be erased at run time
Consider the following dependent data type definition:
data Container : Nat -> Type where
Level : {n : _} -> Container n
The following function compiles:
getLevel : Container n -> Nat
...
1
vote
1
answer
79
views
Proving that user has always less money than bank
I would like to create simple bank application in idris.
I have prepared Bank type:
data Bank : Type where
Init : Bank
Deposit : Bank -> Address -> Nat -> Bank
Withdraw : (s : Bank) -&...
0
votes
1
answer
77
views
How to get normal values from fastPack in Idris?
I am confused about the difference between pack and fastPack functions in Idris2 (as of 0.7.0). Both have the same signature:
:t pack
Prelude.pack : List Char -> String
:t fastPack
Prelude.fastPack ...
thor's user avatar
- 22.8k
0
votes
1
answer
105
views
Erased arguments in type constructors
What does it mean to erase an argument in a type constructor? For example
data Foo : (0 _ : Nat) -> Type where
as opposed to
data Foo : Nat -> Type where
My understanding is that nothing in a ...
0
votes
1
answer
88
views
What does it mean to import a directory in Idris2?
I usually see the import directive in Idris used on a .idr file. But in the code here, I see an instance of import used on a directory.
import public Text.Lexer
, where Text.Lexer is a directory ...
thor's user avatar
- 22.8k
0
votes
1
answer
62
views
Type-safe linear maybeToList
I thought that maybeToList would be a good function to try Idris2's linearity feature on. I'm aware that maybeToVect would usually be a better choice, but I guess that its implementation wouldn't use ...