Skip to main content
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 2 years, 7 months
  • Last seen this week
Profile Activity
Stats
2,353
reputation
12k
reached
21
answers
0
questions
Communities
Badges
View all badges
This user doesn’t have any gold badges yet.
10
silver badges
18
bronze badges
Top tags
View all tags
83
Score
6
Posts
29
Posts %
34
Score
2
Posts
10
Posts %
30
Score
2
Posts
10
Posts %
28
Score
2
Posts
10
Posts %
27
Score
2
Posts
10
Posts %
25
Score
3
Posts
14
Posts %
Top posts
View all questions and answers
answer
26
Why not have `Prop : Set` in Coq?
Jun 27, 2022
answer
20
What exactly is setoid hell?
Mar 1, 2022
answer
19
What is the state of coinductive types and reasoning in Coq?
Feb 15, 2022
answer
16
Incorporating Markov's principle in various proof assistants
Mar 6, 2022
answer
15
What difficulties are there in basing a proof assistant on the $\lambda\mu$-calculus and has any proof assistant tried?
Feb 20, 2022
answer
15
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
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?