refactoring univese to use Prod

mstksg · Aug 4, 2019 · 5f29247 · 5f29247
1 parent 73b7766
commit 5f29247
Show file tree

Hide file tree

Showing 7 changed files with 1,953 additions and 863 deletions.
diff --git a/package.yaml b/package.yaml
@@ -30,7 +30,8 @@ ghc-options:
 
 dependencies:
 - base >= 4.11 && < 5
-- singletons >= 2.4
+- singletons >= 2.5
+- vinyl
 
 library:
   source-dirs: src
diff --git a/src/Data/Type/Predicate/Quantification.hs b/src/Data/Type/Predicate/Quantification.hs
@@ -132,7 +132,8 @@ ientailAllF
     => (forall a. Elem f as a -> p @@ a -> h (q @@ a))    -- ^ implication in context
     -> All f p @@ as
     -> h (All f q @@ as)
-ientailAllF f a = igenAllA (\i _ -> f i (runWitAll a i)) sing
+-- ientailAllF f a = igenAllA (\i _ -> f i (runWitAll a i)) sing
+ientailAllF f a = undefined
 
 -- | If @p@ implies @q@ under some context @h@, and if we have @p a@ for
 -- all @a@, then we must have @q a@ for all @a@ under context @h@.