Data.List.Fresh.Quantifiers.SmartConstructors

Definitions

mkAny : {auto {conArg:5352} : DecEq a} -> (x : a) -> {auto 0 _ : IsYes (isElem x xs)} -> p x -> Any p xs

Totality: total
Visibility: public export

(::) : {auto {conArg:5443} : DecEq a} -> (xpx : (x : a ** p x)) -> {auto 0 pos : IsYes (isElem (xpx .fst) xs)} -> All p (remove (toWitness pos)) -> All p xs

Totality: total
Visibility: public export
Fixity Declaration: infixr operator, level 7