| Copyright | (c) Galois Inc, 2015 |
|---|---|
| License | Apache-2 |
| Maintainer | jhendrix@galois.com, lcasburn@galois.com |
| Safe Haskell | Safe |
| Language | Haskell98 |
Language.Lean.Internal.Typechecker
Contents
Description
Internal declarations for ConstraintSeq and Typechecker.
- data Typechecker
- data ConstraintSeq
- type ConstraintSeqPtr = Ptr ConstraintSeq
- type OutConstraintSeqPtr = Ptr ConstraintSeqPtr
- withConstraintSeq :: ConstraintSeq -> (Ptr ConstraintSeq -> IO a) -> IO a
- type TypecheckerPtr = Ptr Typechecker
- type OutTypecheckerPtr = Ptr TypecheckerPtr
- withTypechecker :: Typechecker -> (Ptr Typechecker -> IO a) -> IO a
Documentation
Foreign exports
type ConstraintSeqPtr = Ptr ConstraintSeq Source
Pointer to lean_cnstr_seq for inputs to Lean functions.
type OutConstraintSeqPtr = Ptr ConstraintSeqPtr Source
Pointer to lean_cnstr_seq for outputs from Lean functions.
withConstraintSeq :: ConstraintSeq -> (Ptr ConstraintSeq -> IO a) -> IO a Source
Get access to lean_cnstr_seq within IO action.
type TypecheckerPtr = Ptr Typechecker Source
Haskell type for lean_type_checker FFI parameters.
type OutTypecheckerPtr = Ptr TypecheckerPtr Source
Haskell type for lean_type_checker* FFI parameters.
withTypechecker :: Typechecker -> (Ptr Typechecker -> IO a) -> IO a Source
Function c2hs uses to pass Typechecker values to Lean