36. Verified membership test
Write contains : Nat → List Nat → Bool and prove contains_spec : ContainsSpec contains: contains x xs is true exactly when x ∈ xs.
There are no tests. The specification pins the function down completely, so a proof of it is worth more than any number of tests.
What the judge checks
contains_spec : ContainsSpec containsThe definitions these names refer to are the read-only lines above the editor. Write any helper lemmas you need before the final theorem.
1def ContainsSpec (f : Nat → List Nat → Bool) : Prop :=
2 ∀ x xs, f x xs = true ↔ x ∈ xs
givenLoading editor…
Type
\to in the editor, or click:Run checks your code against the examples and your custom inputs and records nothing. Submit also runs the hidden tests, confirms the axioms your proof uses and records the result. Each uses one compiler check.
ReadyLn 1, Col 1Lean 4
Draft saved in this browser