Questions tagged [idris]
The idris tag has no usage guidance.
7
questions
0
votes
1
answer
40
views
Is type constraint the same as implication in type space?
In reading idris code, I sometimes wondered what's the mysterious type constraint =>.
It's said that dependent types are a first-class member of Idris. So can be ...
- 2,220
4
votes
2
answers
132
views
Can't infer type for lambda?
I am trying to understand the TinyIdris code for type-checking here. The main function checkTerm handles type inference for lambda abstractions by directing ...
- 2,220
1
vote
0
answers
32
views
How to Show a Term in TinyIdris?
I am trying to follow the code of TinyIdris and print out the basic definitions such as Terms. But I couldn't apply the Show ...
- 2,220
3
votes
1
answer
47
views
How to prove across language boundaries about functions written in another language via FFI?
I know that a proof assistant can prove properties expressed in its own language. However, I find it desirable to call libraries written in other languages when using proof assistants. For example, I'...
- 2,220
2
votes
1
answer
154
views
What is the type-in-type problem in idris2 and can it be avoided?
If I understand it, this video series mentioned that idris2 currently has some type-in-type problems, so that one can exploit it to prove false claims. I am not familiar with the concept, and am ...
- 2,220
8
votes
2
answers
2k
views
Why are these two proofs so different?
I was messing around with toy lemmas in Idris and came up with this silly proof.
...
- 368
3
votes
2
answers
129
views
Multiplicity of implicit type arguments in interfaces
I have the following state monad in Idris 2:
record State (s : Type) (a : Type) where
constructor MkState
run : s -> (s, a)
and I'm trying to define ...
- 1,026