Proof Assistants Beta
gallais's user avatar
gallais's user avatar
gallais's user avatar
gallais
  • Member for 1 year, 10 months
  • Last seen more than a week ago
Profile Activity
Stats
1,106
reputation
6k
reached
16
answers
0
questions
Communities
View all
Badges
View all badges
This user doesn’t have any gold badges yet.
3
silver badges
11
bronze badges
Top tags
View all tags
41
Score
8
Posts
50
Posts %
21
Score
1
Posts
6
Posts %
21
Score
1
Posts
6
Posts %
21
Score
1
Posts
6
Posts %
20
Score
3
Posts
19
Posts %
14
Score
3
Posts
19
Posts %
Top posts
View all questions and answers
All Questions Answers
Score Newest
answer
21
Why should you "never resort to polymorphism when initiality would do"?
Mar 25, 2022
answer
8
Proving uniqueness of an instance of an indexed inductive type
Apr 9, 2022
answer
7
Constructive proof of strong normalization for simply typed lambda calculus
Mar 23, 2022
answer
7
In Agda, why is universe polymorphism explicit?
Mar 23, 2022
answer
7
How to prove f x < f y → x ≢ y
Apr 22
answer
6
Expressivity of mutual/nested inductives vs. regular inductives
Mar 29, 2022
answer
6
Parameterized Datatypes in a Universe à la Tarski?
Mar 22, 2022
answer
5
Proof by Exhaustive Computation for small initial segment of natural numbers (in Coq)
Jul 12, 2022
answer
4
Reasoning about CwFs in a proof assistant
Jun 22
answer
4
Defining a terminating `ripple`, with arguments swapping places
Sep 1
Top network posts
View all network posts
25
How do I verify the Coq proof of Feit-Thompson?
18
Open Type Level Proofs in Haskell/Idris
18
Coq execution difference between semicolon ";" and period "."
17
How to switch the current goal in Coq?
15
What does an apostrophe in front of a list ( '[Something] ) mean in Haskell?

Your privacy

By clicking “Accept all cookies”, you agree Stack Exchange can store cookies on your device and disclose information in accordance with our Cookie Policy.