Stack Exchange

Ana Borges

http://aborges.eu

top accounts reputation activity subscriptions

Top Questions

Has anyone accidentally "proven" a false theorem using what was later found to be a critical bug?

coq reference-request history asked Jul 23, 2022 at 11:04

proofassistants.stackexchange.com

Use results proven in a library (Coq)

coq asked May 19, 2017 at 17:48

stackoverflow.com

Change behaviour of command depending on the presence of a symbol in the input or on the width of the input

conditionals asked Oct 20, 2016 at 19:13

tex.stackexchange.com

Top Answers

How bad is Coq proving both $T$ and $\lnot T$?

mathoverflow.net

How do I turn off the aggressive auto-indent in Proof General/Coq

proofassistants.stackexchange.com

Coq seemingly refuses to recognize a simple substitution of a propositional formula for a propositional variable?

stackoverflow.com

Difference between parameters and members of a class

stackoverflow.com

Naming conventions (letter case, underscores, &c) for Coq

proofassistants.stackexchange.com

Axiomization of Peano arithmetic in constructive first-order logic

proofassistants.stackexchange.com

Building non-classical logics in Agda & Coq

cs.stackexchange.com

To what extent is formalized mathematics publishable?

proofassistants.stackexchange.com

Why does my previously defined function expands/computes to itself?

proofassistants.stackexchange.com