packages feed

lean (empty) → 0.0.0.1

raw patch · 18 files changed

+548/−0 lines, 18 filesdep +basedep +base-unicode-symbolsdep +text-utf8

Dependencies added: base, base-unicode-symbols, text-utf8, transformers, util

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright M Farkas-Dyck © 2019++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of M Farkas-Dyck nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Lean/Exception.hs view
@@ -0,0 +1,25 @@+module Lean.Exception+    (Exception, message, detailedMessage, kind,+     Kind (Null, System, OutOfMemory, Interrupted, Kernel, Parser)) where++import qualified Control.Exception.Base as Base+import Control.Monad+import Data.Text (Text)+import qualified Data.Text as Text+import System.IO.Unsafe++import Lean.IO.Util+import Lean.Raw.C.Exception (Kind)+import qualified Lean.Raw.C.Exception as Raw+import Lean.Wrapper++type Exception = Wrapper Raw.Struct++instance Base.Exception Exception where displayException = Text.unpack . message++message, detailedMessage :: Exception -> Text+message = unsafePerformIO <<< fromRaw <=< Raw.message . unwrap'+detailedMessage = unsafePerformIO <<< fromRaw <=< Raw.detailedMessage . unwrap'++kind :: Exception -> Raw.Kind+kind = Raw.kind . unwrap'
+ Lean/Expr.hs view
@@ -0,0 +1,23 @@+module Lean.Expr (Expr (Lean.Expr.Var, Lean.Expr.Sort)) where++import System.IO.Unsafe++import Lean.Exception ()+import Lean.IO.Util+import qualified Lean.Raw.C.Expr as Raw+import Lean.Wrapper+import Lean.Wrapper.Univ (Univ (Univ))+import qualified Lean.Wrapper.Univ as Univ++newtype Expr = Expr { raw :: Wrapper Raw.Struct }++kindChecked :: Raw.Kind -> (Wrapper Raw.Struct -> IO b) -> Expr -> Maybe b+kindChecked k f = checked ((==) k . Raw.kind) f . raw++pattern Var :: Word -> Expr+pattern Var k <- (kindChecked Raw.Var (liftLean1 Raw.getVarIdx) -> Just k) where+    Var = Expr . unsafePerformIO . liftLean0 . Raw.mkVar . fromIntegral++pattern Sort :: Univ -> Expr+pattern Sort u <- (fmap Univ . kindChecked Raw.Sort (liftLean1 Raw.getSortUniv) -> Just u) where+    Sort = Expr . unsafePerformIO . liftLean1 Raw.mkSort . Univ.raw
+ Lean/IO/Util.hs view
@@ -0,0 +1,66 @@+{-# LANGUAGE TypeFamilies #-}++module Lean.IO.Util where++import Control.Applicative+import Control.Exception.Base+import Control.Monad+import Data.Text (Text)+import qualified Data.Text.Foreign as Text+import Foreign+import Foreign.C.Types+import Foreign.ForeignPtr.Unsafe+import System.IO.Unsafe++import Lean.Wrapper++unwrap' :: Wrapper a -> Ptr a+unwrap' = unsafeForeignPtrToPtr . unwrap++class Storable (Raw a) => FromRaw a where+    type Raw a+    fromRaw :: Raw a -> IO a++instance Drop a => FromRaw (Wrapper a) where+    type Raw (Wrapper a) = Ptr a+    fromRaw = wrap++instance FromRaw Bool where+    type Raw Bool = CInt+    fromRaw = pure . (/= 0)++instance FromRaw Word where+    type Raw Word = CUInt+    fromRaw = pure . fromIntegral++instance FromRaw Int where+    type Raw Int = CInt+    fromRaw = pure . fromIntegral++instance FromRaw Text where+    type Raw Text = Ptr CChar+    fromRaw = getCompose $ Compose (liftA2 (=<<) Text.fromPtr (fmap fromIntegral . cNulArrayLen) . castPtr) <* Compose dropString++foreign import ccall unsafe "lean_string_del" dropString :: Ptr CChar -> IO ()++liftLean0 :: (FromRaw z, Drop ex, Exception (Wrapper ex)) => (Ptr (Raw z) -> Ptr (Ptr ex) -> IO CInt) -> IO z+liftLean0 f = alloca $ \ p -> alloca $ \ q ->+    f p q >>= \ case 0 -> peek q >>= wrap >>= throw; _ -> peek p >>= fromRaw++liftLean1 :: (FromRaw z, Drop ex, Exception (Wrapper ex)) => (Ptr a -> Ptr (Raw z) -> Ptr (Ptr ex) -> IO CInt) -> Wrapper a -> IO z+liftLean1 f a = liftLean0 $ f (unwrap' a)++liftLean2 :: (FromRaw z, Drop ex, Exception (Wrapper ex)) => (Ptr a -> Ptr b -> Ptr (Raw z) -> Ptr (Ptr ex) -> IO CInt) -> Wrapper a -> Wrapper b -> IO z+liftLean2 f a b = liftLean0 $ f (unwrap' a) (unwrap' b)++liftLean3 :: (FromRaw z, Drop ex, Exception (Wrapper ex)) => (Ptr a -> Ptr b -> Ptr c -> Ptr (Raw z) -> Ptr (Ptr ex) -> IO CInt) -> Wrapper a -> Wrapper b -> Wrapper c -> IO z+liftLean3 f a b c = liftLean0 $ f (unwrap' a) (unwrap' b) (unwrap' c)++checked :: (Ptr s -> Bool) -> (Wrapper s -> IO z) -> Wrapper s -> Maybe z+checked pred f s = unsafePerformIO . sequenceA $ f s <$ guard (pred (unwrap' s))++cNulArrayLen :: _ => Ptr a -> IO Word+cNulArrayLen = go 0 where+    go n ptr = peek ptr >>= \ case+        0 -> pure n+        _ -> go (n+1) $ plusPtr ptr 1
+ Lean/Name.hs view
@@ -0,0 +1,39 @@+module Lean.Name where++import Data.Function (on)+import Data.Text (Text)+import qualified Data.Text as Text+import qualified Data.Text.Foreign as Text+import Foreign.Ptr+import System.IO.Unsafe+import Util++import Lean.Exception ()+import Lean.IO.Util+import qualified Lean.Raw.C.Name as Raw+import Lean.Wrapper++newtype Name = Name { raw :: Wrapper Raw.Struct }++instance Show Name where+    show (Name name) = Text.unpack . unsafePerformIO $ liftLean1 Raw.toString name++instance Eq Name where+    Name a == Name b = (/= 0) . unsafePerformIO $ (Raw.eq `on` unwrap') a b++instance Ord Name where+    Name a <= Name b = ((/= 0) . unsafePerformIO $ (Raw.lt `on` unwrap') a b) || Name a == Name b++{-# COMPLETE Anonymous, Str, Idx #-}++pattern Anonymous :: Name+pattern Anonymous <- ((/= 0) . unsafePerformIO . Raw.isAnonymous . unwrap' . raw -> True) where+    Anonymous = Name . unsafePerformIO $ liftLean0 Raw.mkAnonymous++pattern Str :: Name -> Text -> Name+pattern Str name xs <- (checked ((/= 0) . unsafePerformIO . Raw.isStr) (fmap Name . liftLean1 Raw.getPrefix &=& liftLean1 Raw.getStr) . raw -> Just (name, xs)) where+    Str (Name name) = Name . unsafePerformIO . flip Text.useAsPtr (pure . flip (liftLean1 . flip Raw.mkStr) name . castPtr) . flip Text.snoc '\0'++pattern Idx :: Name -> Word -> Name+pattern Idx name k <- (checked ((/= 0) . unsafePerformIO . Raw.isIdx) (fmap Name . liftLean1 Raw.getPrefix &=& liftLean1 Raw.getIdx) . raw -> Just (name, k)) where+    Idx (Name name) = Name . unsafePerformIO . flip (liftLean1 . flip Raw.mkIdx) name . fromIntegral
+ Lean/Raw/C/Decl.hsc view
@@ -0,0 +1,34 @@+module Lean.Raw.C.Decl where++import Foreign+import Foreign.C.Types++import qualified Lean.Raw.C.Decl.Cert as Cert+import Lean.Raw.C.Env (Env)+import Lean.Raw.C.Exception (Exception)+import Lean.Raw.C.Expr (Expr)+import Lean.Raw.C.Name (ListName, Name)+import Lean.Wrapper++#include <lean.h>++newtype Kind = Kind CInt+  deriving (Eq)++#{enum Kind, Kind,+  Const = LEAN_DECL_CONST,+  Axiom = LEAN_DECL_AXIOM,+  Def   = LEAN_DECL_DEF,+  Thm   = LEAN_DECL_THM}++data Struct++instance Drop Struct where drop = drop'+foreign import ccall unsafe "&lean_decl_del" drop' :: FunPtr (Ptr Struct -> IO ())++type Decl = Ptr Struct++foreign import ccall unsafe "lean_decl_mk_axiom" mkAxiom :: Name -> ListName -> Expr -> Ptr Decl -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_decl_mk_const" mkConst :: Name -> ListName -> Expr -> Ptr Decl -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_decl_mk_def_with" mkDef :: Env -> Name -> ListName -> Expr -> Expr -> CUInt -> CInt -> Ptr Decl -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_decl_check" check :: Env -> Decl -> Ptr Cert.Decl -> Ptr Exception -> IO CInt
+ Lean/Raw/C/Decl/Cert.hsc view
@@ -0,0 +1,14 @@+module Lean.Raw.C.Decl.Cert where++import Foreign++import Lean.Wrapper++#include <lean.h>++data Struct++instance Drop Struct where drop = drop'+foreign import ccall unsafe "&lean_cert_decl_del" drop' :: FunPtr (Ptr Struct -> IO ())++type Decl = Ptr Struct
+ Lean/Raw/C/Env.hsc view
@@ -0,0 +1,21 @@+module Lean.Raw.C.Env where++import Foreign+import Foreign.C.Types++import qualified Lean.Raw.C.Decl.Cert as Cert (Decl)+import Lean.Raw.C.Exception (Exception)+import Lean.Wrapper++#include <lean.h>++data Struct++instance Drop Struct where drop = drop'+foreign import ccall unsafe "&lean_env_del" drop' :: FunPtr (Ptr Struct -> IO ())++type Env = Ptr Struct++foreign import ccall unsafe "lean_env_mk_std" mkStd :: CUInt -> Ptr Env -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_env_add" add :: Env -> Cert.Decl -> Ptr Env -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_env_replace" replace :: Env -> Cert.Decl -> Ptr Env -> Ptr Exception -> IO CInt
+ Lean/Raw/C/Exception.hsc view
@@ -0,0 +1,30 @@+module Lean.Raw.C.Exception where++import Foreign+import Foreign.C.Types++import Lean.Wrapper++#include <lean.h>++data Struct++instance Drop Struct where drop = drop'+foreign import ccall unsafe "&lean_exception_del" drop' :: FunPtr (Ptr Struct -> IO ())++type Exception = Ptr Struct++newtype Kind = Kind CInt+  deriving (Eq)++#{enum Kind, Kind,+  Null        = LEAN_NULL_EXCEPTION,+  System      = LEAN_SYSTEM_EXCEPTION,+  OutOfMemory = LEAN_OUT_OF_MEMORY,+  Interrupted = LEAN_INTERRUPTED,+  Kernel      = LEAN_KERNEL_EXCEPTION,+  Parser      = LEAN_PARSER_EXCEPTION}++foreign import ccall unsafe "lean_exception_get_message" message :: Exception -> IO (Ptr CChar)+foreign import ccall unsafe "lean_exception_get_detailed_message" detailedMessage :: Exception -> IO (Ptr CChar)+foreign import ccall unsafe "lean_exception_get_kind" kind :: Exception -> Kind
+ Lean/Raw/C/Expr.hsc view
@@ -0,0 +1,40 @@+module Lean.Raw.C.Expr where++import Foreign+import Foreign.C.Types++import Lean.Raw.C.Exception (Exception)+import Lean.Raw.C.Univ (Univ)+import Lean.Wrapper++#include <lean.h>++data Struct++instance Drop Struct where drop = drop'+foreign import ccall unsafe "&lean_expr_del" drop' :: FunPtr (Ptr Struct -> IO ())++type Expr = Ptr Struct++newtype Kind = Kind CInt+  deriving (Eq)++#{enum Kind, Kind,+  Var    = LEAN_EXPR_VAR,+  Sort   = LEAN_EXPR_SORT,+  Const  = LEAN_EXPR_CONST,+  Local  = LEAN_EXPR_LOCAL,+  Meta   = LEAN_EXPR_META,+  App    = LEAN_EXPR_APP,+  Lambda = LEAN_EXPR_LAMBDA,+  Pi     = LEAN_EXPR_PI,+  Let    = LEAN_EXPR_LET,+  Macro  = LEAN_EXPR_MACRO}++foreign import ccall unsafe "lean_expr_mk_var" mkVar :: CUInt -> Ptr Expr -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_expr_mk_sort" mkSort :: Univ -> Ptr Expr -> Ptr Exception -> IO CInt++foreign import ccall unsafe "lean_expr_get_var_idx" getVarIdx :: Expr -> Ptr CUInt -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_expr_get_sort_univ" getSortUniv :: Expr -> Ptr Univ -> Ptr Exception -> IO CInt++foreign import ccall unsafe "lean_expr_kind" kind :: Expr -> Kind
+ Lean/Raw/C/Name.hsc view
@@ -0,0 +1,41 @@+module Lean.Raw.C.Name where++import Foreign+import Foreign.C.Types++import Lean.Raw.C.Exception (Exception)+import Lean.Wrapper++#include <lean.h>++data Struct++instance Drop Struct where drop = drop'+foreign import ccall unsafe "&lean_name_del" drop' :: FunPtr (Ptr Struct -> IO ())++type Name = Ptr Struct++foreign import ccall unsafe "lean_name_del" drop :: Name -> IO ()+foreign import ccall unsafe "lean_name_mk_anonymous" mkAnonymous :: Ptr Name -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_name_mk_str" mkStr :: Name -> Ptr CChar -> Ptr Name -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_name_mk_idx" mkIdx :: Name -> CUInt -> Ptr Name -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_name_eq" eq :: Name -> Name -> IO CInt+foreign import ccall unsafe "lean_name_lt" lt :: Name -> Name -> IO CInt+foreign import ccall unsafe "lean_name_to_string" toString :: Name -> Ptr (Ptr CChar) -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_name_is_anonymous" isAnonymous :: Name -> IO CInt+foreign import ccall unsafe "lean_name_is_str" isStr :: Name -> IO CInt+foreign import ccall unsafe "lean_name_is_idx" isIdx :: Name -> IO CInt+foreign import ccall unsafe "lean_name_get_prefix" getPrefix :: Name -> Ptr Name -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_name_get_str" getStr :: Name -> Ptr (Ptr CChar) -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_name_get_idx" getIdx :: Name -> Ptr CUInt -> Ptr Exception -> IO CInt++data ListStruct++type ListName = Ptr ListStruct++foreign import ccall unsafe "lean_list_name_del" dropList :: ListName -> IO ()+foreign import ccall unsafe "lean_list_name_mk_nil" mkNil :: Ptr ListName -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_list_name_mk_cons" mkCons :: Name -> ListName -> Ptr ListName -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_list_name_eq" eqList :: ListName -> ListName -> IO CInt+foreign import ccall unsafe "lean_list_name_head" head :: ListName -> Ptr Name -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_list_name_del" tail :: ListName -> Ptr ListName -> Ptr Exception -> IO CInt
+ Lean/Raw/C/Univ.hsc view
@@ -0,0 +1,43 @@+module Lean.Raw.C.Univ where++import Foreign+import Foreign.C.Types++import Lean.Raw.C.Exception (Exception)+import Lean.Raw.C.Name (Name)+import Lean.Wrapper++#include <lean.h>++data Struct++instance Drop Struct where drop = drop'+foreign import ccall unsafe "&lean_univ_del" drop' :: FunPtr (Ptr Struct -> IO ())++type Univ = Ptr Struct++foreign import ccall unsafe "lean_univ_mk_zero" mkZero :: Ptr Univ -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_univ_mk_succ" mkSucc :: Univ -> Ptr Univ -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_univ_mk_max"  mkMax  :: Univ -> Univ -> Ptr Univ -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_univ_mk_imax" mkImax :: Univ -> Univ -> Ptr Univ -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_univ_mk_param" mkParam :: Name -> Ptr Univ -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_univ_mk_meta" mkMeta :: Name -> Ptr Univ -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_univ_eq" eq :: Univ -> Univ -> Ptr CInt -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_univ_lt" lt :: Univ -> Univ -> Ptr CInt -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_univ_get_pred" getPred :: Univ -> Ptr Univ -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_univ_get_max_lhs" getMaxLhs :: Univ -> Ptr Univ -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_univ_get_max_rhs" getMaxRhs :: Univ -> Ptr Univ -> Ptr Exception -> IO CInt+foreign import ccall unsafe "lean_univ_get_name" getName :: Univ -> Ptr Name -> Ptr Exception -> IO CInt++newtype Kind = Kind CInt+  deriving (Eq)++#{enum Kind, Kind,+  Zero  = LEAN_UNIV_ZERO,+  Succ  = LEAN_UNIV_SUCC,+  Max   = LEAN_UNIV_MAX,+  Imax  = LEAN_UNIV_IMAX,+  Param = LEAN_UNIV_PARAM,+  Meta  = LEAN_UNIV_META}++foreign import ccall unsafe "lean_univ_kind" kind :: Univ -> Kind
+ Lean/Univ.hs view
@@ -0,0 +1,49 @@+module Lean.Univ (Univ (Lean.Univ.Zero, Lean.Univ.Succ, Lean.Univ.Max, Lean.Univ.Imax, Lean.Univ.Param, Lean.Univ.Meta)) where++import Control.Arrow ((***))+import Foreign.Ptr+import System.IO.Unsafe+import Util++import Lean.IO.Util+import Lean.Exception ()+import Lean.Name (Name (Name))+import qualified Lean.Name as Name+import qualified Lean.Raw.C.Univ as Raw+import Lean.Wrapper.Univ++instance FromRaw Univ where+    type Raw Univ = Ptr Raw.Struct+    fromRaw = fmap Univ . fromRaw++instance Eq Univ where+    Univ a == Univ b = unsafePerformIO $ liftLean2 Raw.eq a b++instance Ord Univ where+    Univ a <= Univ b = (unsafePerformIO $ liftLean2 Raw.lt a b) || Univ a == Univ b++{-# COMPLETE Zero, Succ, Max, Imax, Param, Meta #-}++pattern Zero :: Univ+pattern Zero <- (Raw.kind . unwrap' . raw -> Raw.Zero) where+    Zero = Univ . unsafePerformIO $ liftLean0 Raw.mkZero++pattern Succ :: Univ -> Univ+pattern Succ u <- (fmap Univ . checked ((==) Raw.Succ . Raw.kind) (liftLean1 Raw.getPred) . raw -> Just u) where+    Succ = Univ . unsafePerformIO . liftLean1 Raw.mkSucc . raw++pattern Max :: Univ -> Univ -> Univ+pattern Max u v <- (fmap (Univ *** Univ) . checked ((==) Raw.Max . Raw.kind) (liftLean1 Raw.getMaxLhs &=& liftLean1 Raw.getMaxRhs) . raw -> Just (u, v)) where+    Max = curry $ Univ . unsafePerformIO . \ (Univ u, Univ v) -> liftLean2 Raw.mkMax u v++pattern Imax :: Univ -> Univ -> Univ+pattern Imax u v <- (fmap (Univ *** Univ) . checked ((==) Raw.Imax . Raw.kind) (liftLean1 Raw.getMaxLhs &=& liftLean1 Raw.getMaxRhs) . raw -> Just (u, v)) where+    Imax = curry $ Univ . unsafePerformIO . \ (Univ u, Univ v) -> liftLean2 Raw.mkImax u v++pattern Param :: Name -> Univ+pattern Param name <- (fmap Name . checked ((==) Raw.Param . Raw.kind) (liftLean1 Raw.getName) . raw -> Just name) where+    Param = Univ . unsafePerformIO . liftLean1 Raw.mkParam . Name.raw++pattern Meta :: Name -> Univ+pattern Meta name <- (fmap Name . checked ((==) Raw.Meta . Raw.kind) (liftLean1 Raw.getName) . raw -> Just name) where+    Meta = Univ . unsafePerformIO . liftLean1 Raw.mkMeta . Name.raw
+ Lean/Wrapper.hs view
@@ -0,0 +1,12 @@+module Lean.Wrapper where++import Foreign++class Drop a where+    drop :: FunPtr (Ptr a -> IO ())++newtype Wrapper a = Wrapper { unwrap :: ForeignPtr a }+  deriving (Show)++wrap :: Drop a => Ptr a -> IO (Wrapper a)+wrap = fmap Wrapper . newForeignPtr drop
+ Lean/Wrapper/Univ.hs view
@@ -0,0 +1,6 @@+module Lean.Wrapper.Univ where++import qualified Lean.Raw.C.Univ as Raw+import Lean.Wrapper++newtype Univ = Univ { raw :: Wrapper Raw.Struct }
+ Prelude.hs view
@@ -0,0 +1,7 @@+{-# LANGUAGE PackageImports #-}++module Prelude (module A) where++import "base" Prelude as A hiding (drop, id, (.))+import Control.Category as A+import Data.Functor.Compose as A
+ README.md view
@@ -0,0 +1,1 @@+# lean
+ lean.cabal view
@@ -0,0 +1,67 @@+name:                lean+version:             0.0.0.1+synopsis:            Bonds to Lean theorem prover+-- description:+license:             BSD3+license-file:        LICENSE+author:              M Farkas-Dyck+maintainer:          strake888@gmail.com+copyright:           2019 M Farkas-Dyck+category:            Math+build-type:          Simple+extra-source-files:  README.md+cabal-version:       >=1.10++library+  hs-source-dirs:      .+  exposed-modules:     Lean.Exception+                     , Lean.Expr+                     , Lean.Name+                     , Lean.Univ+                     , Lean.Raw.C.Decl+                     , Lean.Raw.C.Decl.Cert+                     , Lean.Raw.C.Env+                     , Lean.Raw.C.Exception+                     , Lean.Raw.C.Expr+                     , Lean.Raw.C.Name+                     , Lean.Raw.C.Univ+  other-modules:       Prelude+                     , Lean.IO.Util+                     , Lean.Wrapper+                     , Lean.Wrapper.Univ+  build-depends:       base >= 4.7 && < 5+                     , base-unicode-symbols+                     , text-utf8+                     , transformers+                     , util+  default-language:    Haskell2010+  default-extensions:  UnicodeSyntax+                     , LambdaCase+                     , EmptyCase+                     , InstanceSigs+                     , PartialTypeSignatures+                     , PatternSynonyms+                     , ViewPatterns+                     , PolyKinds+                     , ConstraintKinds+                     , FlexibleContexts+                     , FlexibleInstances+                     , TypeFamilies+                     , MonadComprehensions+                     , StandaloneDeriving+                     , GeneralizedNewtypeDeriving+                     , DeriveFunctor, DeriveFoldable, DeriveTraversable+  ghc-options:         -Wall -Wcompat -Wredundant-constraints -Wno-name-shadowing+                       -Wincomplete-record-updates -Wincomplete-uni-patterns+                       -Werror=incomplete-patterns+                       -Werror=incomplete-uni-patterns+                       -Werror=incomplete-record-updates+                       -Werror=missing-fields+                       -Werror=missing-methods+                       -Wno-partial-type-signatures+                       -Wno-orphans+  build-tools:         hsc2hs++source-repository head+  type:     git+  location: https://github.com/strake/lean.hs