Questions tagged [examples]
The examples tag has no usage guidance.
4
questions
1
vote
1
answer
69
views
Inductive types associated to instances of a structure in Lean
I am using the Lean computer proof assistant. I am using the combinatorial structure of a graph with an abelian operation on its edges as a learning example.
In it I have a structure Graph. I want to ...
- 73
1
vote
1
answer
79
views
How do I prove this property in Coq?
I am working on a variant of an example by Christine Paulin-Mohring. It represents in Coq the Needham-Schroeder protocol in the (flawed) public key version. I would like to prove that the protocol is ...
- 135
6
votes
1
answer
276
views
What are some good (bad) examples of "green slime"?
I know what this roughly is. But when I'm explaining to a friend, I have trouble pulling out examples from my head. Are there any minimal working examples (maybe "minimal non-working examples&...
- 2,916
3
votes
0
answers
71
views
What are some "real world" first order logical theories for demos?
I'm working on a tool for first order logical theories. I want to show the tool can work with real world logical theories. What are some good theories for demos?
I think I want demos that are:
...
- 2,422