
  0 | module Data.List.Fresh.Quantifiers.SmartConstructors
  1 | 
  2 | import Data.List.Fresh
  3 | import Data.List.Fresh.Quantifiers
  4 | 
  5 | import Decidable.Decidable.Extra1
  6 | import Decidable.Equality
  7 | 
  8 | %default total
  9 | 
 10 | public export
 11 | mkAny : DecEq a => (x : a) -> {xs : FreshList a neq} ->
 12 |         {auto 0 pos : IsYes (x `isElem` xs)} ->
 13 |         p x -> Any p xs
 14 | mkAny x px = map (\x, Refl => px) (toWitness pos)
 15 | 
 16 | public export
 17 | (::) : DecEq a =>
 18 |          (xpx : (x : a ** p x)) -> {xs : FreshList a neq} ->
 19 |          {auto 0 pos : IsYes (xpx.fst `isElem` xs)} ->
 20 |          All p (remove (toWitness pos)) -> All p xs
 21 | (x ** px) :: pxs = insertWith (\y, Refl => px) (toWitness pos) pxs
 22 |