Questions tagged [idris]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
0 votes
1 answer
36 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 ...
tinlyx's user avatar
  • 1,896
4 votes
2 answers
69 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 ...
tinlyx's user avatar
  • 1,896
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 ...
tinlyx's user avatar
  • 1,896
3 votes
1 answer
46 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'...
tinlyx's user avatar
  • 1,896
2 votes
1 answer
118 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 ...
tinlyx's user avatar
  • 1,896
7 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. ...
Nathan's user avatar
  • 358
3 votes
2 answers
123 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 ...
ionchy's user avatar
  • 1,026