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
83
What are the strengths and weaknesses of the Isabelle proof assistant compared to Coq?
stackoverflow.com

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

21
What does "Error: Universe inconsistency" mean in Coq?
stackoverflow.com

18
What exactly is a Set in Coq
stackoverflow.com

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

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

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

13
Coq: typeclasses vs dependent records
stackoverflow.com

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

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

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

11
Inversion produces unexpected existT in Coq
stackoverflow.com

11
How to duplicate a hypothesis in Coq?
stackoverflow.com

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

11
Difference between Definition and Let in Coq
stackoverflow.com

11
Como traduzir "De Londres com carinho"?
portuguese.stackexchange.com

10
Is it possible to write C programs using Coq?
stackoverflow.com

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

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

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

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

9
How to do "negative" match in Ltac?
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

8
Distinção entre falo/falo/fá-lo
portuguese.stackexchange.com

8
If it is impossible to have O(1) pred on CoC, then why does this work?
stackoverflow.com

8
Problem "<dead-acute> is undefined" appearing when typing Greek stress ( ' )
emacs.stackexchange.com

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

8
How do we know all Coq constructors are injective and disjoint?
stackoverflow.com

1 2 3 4