Proof Assistants Beta
Pierre-Marie Pédrot's user avatar
Pierre-Marie Pédrot's user avatar
Pierre-Marie Pédrot's user avatar
Pierre-Marie Pédrot
  • Member for 1 year
  • Last seen this week
Profile Activity
Stats
2,166
reputation
7k
reached
20
answers
0
questions
top 7% overall
Communities
Badges
View all badges
This user doesn’t have any gold badges yet.
8
silver badges
17
bronze badges
Top tags
View all tags
68
Score
5
Posts
25
Posts %
29
Score
2
Posts
10
Posts %
27
Score
2
Posts
10
Posts %
26
Score
2
Posts
10
Posts %
24
Score
3
Posts
15
Posts %
23
Score
2
Posts
10
Posts %
Top posts
View all questions and answers
All Questions Answers
Score Newest
answer
21
Why not have `Prop : Set` in Coq?
Jun 27, 2022
answer
16
What is the state of coinductive types and reasoning in Coq?
Feb 15, 2022
answer
15
What exactly is setoid hell?
Mar 1, 2022
answer
15
Incorporating Markov's principle in various proof assistants
Mar 6, 2022
answer
14
What axioms have a computational interpretation?
Mar 8, 2022
answer
13
Is there any example of a dependent product that makes sense in a non-type-theory context?
Mar 20, 2022
answer
13
What difficulties are there in basing a proof assistant on the $\lambda\mu$-calculus and has any proof assistant tried?
Feb 20, 2022
answer
11
What axioms do I need to search the naturals?
Apr 24, 2022
answer
10
What's the difference between a universe level and a natural number?
Feb 20, 2022
answer
9
Can a proof engine be built based on graphs?
Feb 28, 2022
Top network posts
View all network posts
7
What is the runtime/time complexity of Coq’s (Dependent) Type Inference?

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.