Commit 1cbda487 authored by Robbert Krebbers's avatar Robbert Krebbers

Type class version of `elem_of` for lists.

parent 149f5aa7
Pipeline #13180 passed with stage
in 8 minutes and 32 seconds
......@@ -129,6 +129,13 @@ Existing Class TCForall2.
Existing Instance TCForall2_nil.
Existing Instance TCForall2_cons.
Inductive TCElemOf {A} (x : A) : list A Prop :=
| TCElemOf_here xs : TCElemOf x (x :: xs)
| TCElemOf_further y xs : TCElemOf x xs TCElemOf x (y :: xs).
Existing Class TCElemOf.
Existing Instance TCElemOf_here.
Existing Instance TCElemOf_further.
Inductive TCEq {A} (x : A) : A Prop := TCEq_refl : TCEq x x.
Existing Class TCEq.
Existing Instance TCEq_refl.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment