Questions tagged [big-list]
Questions designed to generate a "big list" of certain results, examples, conjectures, etc. via many individual answers, each contributing one or a few instances. If the question is not objective consider the tag soft-question.
3 questions
4
votes
4
answers
771
views
Defining a terminating `ripple`, with arguments swapping places
In Agda, I can make the following definition, and Agda believes that the recursion terminates.
Notice that the arguments “swap places” in the recursive call, so neither of the arguments individually ...
- 1,063
3
votes
4
answers
241
views
What provers are using quote, quotations or quasiquotations?
This is a related question to
Is there a consolidated or partial list noting the use of quasiquotation with provers?
for which it seems there is no answer. However as there might be an answer some ...
- 2,856
17
votes
7
answers
989
views
What are some examples of proof assistants doing something useful? [closed]
I know that Proof Assistants can be used in fact-checking, but what else can they be used for? How would they be used for specific roles, including industry jobs and everyday life?
- 1,348