Stack Exchange

Arthur Azevedo De Amorim

Philadelphia, PA

http://cis.upenn.edu/~arthuraa

I have a blog (http://poleiro.info) about the Coq proof assistant, please check it out!

top accounts reputation activity bookmarks subscriptions
Top Questions
Top Answers
67
What are the strengths and weaknesses of the Isabelle proof assistant compared to Coq?
stackoverflow.com

20
Why are logical connectives and booleans separate in Coq?
stackoverflow.com

18
What does “Error: Universe inconsistency” mean in Coq?
stackoverflow.com

15
Coq QArith division by zero is zero, why?
stackoverflow.com

15
What exactly is a Set in COQ
stackoverflow.com

13
Quando, como e porque a língua portuguesa foi dividida?
portuguese.stackexchange.com

12
How or is that possible to prove or falsify `forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.` in Coq?
stackoverflow.com

12
Coq: typeclasses vs dependent records
stackoverflow.com

12
How do I read the definition of ex_intro?
stackoverflow.com

11
Difference between Definition and Let in Coq
stackoverflow.com

11
Como traduzir “De Londres com carinho”?
portuguese.stackexchange.com

11
Qual é a tradução de “statement” dentro do âmbito da programação?
portuguese.stackexchange.com

10
How to introduce a new variable in Coq?
stackoverflow.com

10
Quais os usos mais comuns de “barriga”, “pança”, “papo”, “abdômen” e “ventre” em uma frase?
portuguese.stackexchange.com

9
Inversion produces unexpected existT in Coq
stackoverflow.com

9
Why Coq doesn't allow inversion, destruct, etc. when the goal is a Type?
stackoverflow.com

9
How to forbid simpl tactic to unfold arithmetic expressions?
stackoverflow.com

9
How to match a “match” expression?
stackoverflow.com

9
How to prove False from obviously contradictory assumptions
stackoverflow.com

9
Relação entre as palavras “filho” e “fio”
portuguese.stackexchange.com

9
Fail to use let-destruct for tuple in Coq
stackoverflow.com

9
Why is it impossible to perform induction on a term that is used in conclusion?
stackoverflow.com

8
Returning a record from a definition in Coq
stackoverflow.com

8
How to prove “~(nat = False)”, “~(nat = bool)” and “~(nat = True)” in coq
stackoverflow.com

8
Canonical structures in ssreflect
stackoverflow.com

8
Equal indexed inductive types implies equal indices
stackoverflow.com

8
Proofs' role in Coq extractions
stackoverflow.com

8
How to do “negative” match in Ltac?
stackoverflow.com

8
Ltac pattern matching: why does `forall x, ?P x` not match `forall x, x`?
stackoverflow.com

8
Nested recursion and `Program Fixpoint` or `Function`
stackoverflow.com

1 2 3 4