Submission Details

Back to Submissions List

Challenge: isIn

Submitted by: Violeta Hernández Palacios

Submitted at: 2024-11-19 09:39:54

Code:

def isIn (x:Int) (xs: List Int):Bool
:= xs.contains x

First Theorem Proof:

def isIn_correct (x:Int)(xs:List Int):
  isIn x xs = true ↔ x∈ xs
:= by simp [isIn]

Status: Correct

Feedback: