45 questions
- Bountied 0
- Unanswered
- Frequent
- Score
- Trending
- Week
- Month
- Unanswered (my tags)
1
vote
1
answer
39
views
Why does the error "patterns require matching on different types" when using lazy lists Nil and (::)?
This works in Idris 2 :
intersperse : a -> LazyList a -> LazyList a
intersperse _ Nil = Nil
intersperse _ (x :: Nil) = x :: Nil
intersperse sep (x :: y :: xs) = x :: sep :: ...
0
votes
1
answer
55
views
Convert Vect AnyPtr to C Array (AnyPtr) in Idris 2
I am writing bindings for the Z3 solver library for Idris, but have gotten stuck because I can't seem to find a way to pass a Vect AnyPtr to a Z3 function (in this case, Z3_mk_and with signature ...
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 ...
0
votes
0
answers
47
views
Why does Idris2 not reduce this function call within the type?
I expected lemma4 to reduce so that Refl would work but when trying that I get Error: While processing right hand side of lemma4. Can't solve constraint between: [p] and expanded_shape (DimSame Scalar ...
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 ...
1
vote
0
answers
101
views
Type level palindrome check in Idris
I'm learning Idris and decided to do it by contributing to the Rosetta code. First task, implementing a palindrome checker. I have implemented several versions for run-time checking and one simple ...
1
vote
0
answers
26
views
Get list of data constructors in Idris 2
I want to get a list of data constructors in Idris 2. How is this done?
This seems to work, but is there a better way to do this?
module GetConstructors
import Language.Reflection
%language ...
0
votes
1
answer
40
views
Transpose Vector Matrix in Idris2 With Dependant Types
I have trouble figuring out what my Idris2 Type- or Compile-Error is about, so I thought I could ask some Idris2 Veterans or Enthusiasts to give me some explanation on how I can make my approach work ...
2
votes
0
answers
125
views
Prove isomorphism between naturals and their Boehm-Berarducci encoding
I can't figure out how to prove this isomorphism. Intuitively it holds, because the only way to combine the zero parameter and the successor parameter is to apply the successor parameter a few times ...
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
65
views
Prove max x y = y given that x <= y in Idris 2?
I am new to Idris2 and need some guidance on proving the following relationship:
simplify_max : (LTE x y) -> (max x y) = y
simplify_max prf = ?code
I read in the docs that the constructors for LTE ...
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