lean-bindings-0.1: Haskell bindings to the Lean Theorem Prover.

Copyright(c) Galois Inc, 2015
LicenseApache-2
Maintainerjhendrix@galois.com, lcasburn@galois.com
Safe HaskellSafe
LanguageHaskell98

Language.Lean.Internal.Decl

Contents

Description

Declares internal datatypes for Lean environment, declarations, and certified declarations.

Synopsis

Environment

newtype Env Source

A Lean environment

Constructors

Env (ForeignPtr Env) 

Instances

type EnvPtr = Ptr Env Source

Haskell type for lean_env FFI parameters.

type OutEnvPtr = Ptr EnvPtr Source

Haskell type for lean_env* FFI parameters.

withEnv :: Env -> (Ptr Env -> IO a) -> IO a Source

Function c2hs uses to pass Env values to Lean

Declaration

data Decl Source

A Lean declaration

Instances

type DeclPtr = Ptr Decl Source

Haskell type for lean_decl FFI parameters.

type OutDeclPtr = Ptr DeclPtr Source

Haskell type for lean_decl* FFI parameters.

withDecl :: Decl -> (Ptr Decl -> IO a) -> IO a Source

Function c2hs uses to pass Decl values to Lean

Certified declaration

data CertDecl Source

A Lean certified declaration

Instances

type CertDeclPtr = Ptr CertDecl Source

Haskell type for lean_cert_decl FFI parameters.

type OutCertDeclPtr = Ptr CertDeclPtr Source

Haskell type for lean_cert_decl* FFI parameters.

withCertDecl :: CertDecl -> (Ptr CertDecl -> IO a) -> IO a Source

Function c2hs uses to pass CertDecl values to Lean