gallais's user avatar
gallais's user avatar
gallais's user avatar
gallais
  • Member for 2 years
  • Last seen more than a month ago
21 votes
Accepted

Why should you "never resort to polymorphism when initiality would do"?

8 votes

Proving uniqueness of an instance of an indexed inductive type

7 votes

Constructive proof of strong normalization for simply typed lambda calculus

7 votes

In Agda, why is universe polymorphism explicit?

7 votes
Accepted

How to prove f x < f y → x ≢ y

6 votes
Accepted

Parameterized Datatypes in a Universe à la Tarski?

6 votes

Expressivity of mutual/nested inductives vs. regular inductives

5 votes

Proof by Exhaustive Computation for small initial segment of natural numbers (in Coq)

4 votes

Reasoning about CwFs in a proof assistant

4 votes

Defining a terminating `ripple`, with arguments swapping places

4 votes
Accepted

Literate Agda: How do I change the size of the displayed code?

3 votes

Tutorial implementations of NbE

3 votes

Multiplicity of implicit type arguments in interfaces

3 votes

Proving strict positivity in Agda

3 votes
Accepted

Agda - Help with importing Haskell function via FFI

2 votes

How to prove that addition is commutative for conatural numbers in Coq