Questions tagged [examples]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
1 vote
2 answers

How do I define a function in Coq with if...then..else behavior?

I am still a beginner in Coq, so perhaps my issue is trivial but I was unable to find a solution by searching the documentation available online. I am defining in Coq the syntax of a programming ...
Pietro Braione's user avatar
1 vote
1 answer

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 ...
Ronald J. Zallman's user avatar
1 vote
1 answer

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 ...
Pietro Braione's user avatar
10 votes
1 answer

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&...
Trebor's user avatar
  • 3,738
3 votes
0 answers

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: ...
Molly Stewart-Gallus's user avatar