-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A tiny language for understanding the lambda-calculus
--   
--   elsa is a small proof checker for verifying sequences of reductions of
--   lambda-calculus terms. The goal is to help students build up intuition
--   about lambda-terms, alpha-equivalence, beta-reduction, and in general,
--   the notion of computation by substitution.
@package elsa
@version 0.2.1.2

module Language.Elsa.Types
type Id = String
type SElsa = Elsa SourceSpan
type SDefn = Defn SourceSpan
type SExpr = Expr SourceSpan
type SEval = Eval SourceSpan
type SStep = Step SourceSpan
type SBind = Bind SourceSpan
type SEqn = Eqn SourceSpan
type SResult = Result SourceSpan

-- | Result
data Result a
OK :: Bind a -> Result a
Partial :: Bind a -> a -> Result a
Invalid :: Bind a -> a -> Result a
Unbound :: Bind a -> Id -> a -> Result a
failures :: [Result a] -> [Id]
successes :: [Result a] -> [Id]
resultError :: Located a => Result a -> Maybe UserError
mkErr :: Located a => a -> Text -> Maybe UserError

-- | Programs
data Elsa a
Elsa :: [Defn a] -> [Eval a] -> Elsa a
[defns] :: Elsa a -> [Defn a]
[evals] :: Elsa a -> [Eval a]
data Defn a
Defn :: !Bind a -> !Expr a -> Defn a
data Eval a
Eval :: !Bind a -> !Expr a -> [Step a] -> Eval a
[evName] :: Eval a -> !Bind a
[evRoot] :: Eval a -> !Expr a
[evSteps] :: Eval a -> [Step a]
data Step a
Step :: !Eqn a -> !Expr a -> Step a
data Eqn a
AlphEq :: a -> Eqn a
BetaEq :: a -> Eqn a
UnBeta :: a -> Eqn a
DefnEq :: a -> Eqn a
TrnsEq :: a -> Eqn a
UnTrEq :: a -> Eqn a
NormEq :: a -> Eqn a
data Bind a
Bind :: Id -> a -> Bind a
data Expr a
EVar :: Id -> a -> Expr a
ELam :: !Bind a -> !Expr a -> a -> Expr a
EApp :: !Expr a -> !Expr a -> a -> Expr a
data RExpr
RVar :: Id -> RExpr
RLam :: Id -> RExpr -> RExpr
RApp :: RExpr -> RExpr -> RExpr
rExpr :: Expr a -> RExpr
bkLam :: Expr a -> ([Bind a], Expr a)
mkLam :: Monoid a => [Bind a] -> Expr a -> Expr a
bindId :: Bind a -> Id

-- | Tag Extraction
class Tagged t
tag :: Tagged t => t a -> a
instance GHC.Generics.Generic Language.Elsa.Types.RExpr
instance GHC.Classes.Eq Language.Elsa.Types.RExpr
instance GHC.Show.Show a => GHC.Show.Show (Language.Elsa.Types.Elsa a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Language.Elsa.Types.Elsa a)
instance GHC.Show.Show a => GHC.Show.Show (Language.Elsa.Types.Defn a)
instance GHC.Classes.Eq (Language.Elsa.Types.Defn a)
instance GHC.Show.Show a => GHC.Show.Show (Language.Elsa.Types.Eval a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Language.Elsa.Types.Eval a)
instance GHC.Show.Show a => GHC.Show.Show (Language.Elsa.Types.Step a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Language.Elsa.Types.Step a)
instance GHC.Base.Functor Language.Elsa.Types.Result
instance GHC.Show.Show a => GHC.Show.Show (Language.Elsa.Types.Result a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Language.Elsa.Types.Result a)
instance GHC.Base.Functor Language.Elsa.Types.Bind
instance GHC.Show.Show a => GHC.Show.Show (Language.Elsa.Types.Bind a)
instance GHC.Show.Show a => GHC.Show.Show (Language.Elsa.Types.Eqn a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Language.Elsa.Types.Eqn a)
instance Language.Elsa.Types.Tagged Language.Elsa.Types.Eqn
instance Language.Elsa.Types.Tagged Language.Elsa.Types.Bind
instance Language.Elsa.Types.Tagged Language.Elsa.Types.Expr
instance Data.Hashable.Class.Hashable Language.Elsa.Types.RExpr
instance GHC.Show.Show (Language.Elsa.Types.Expr a)
instance GHC.Classes.Eq (Language.Elsa.Types.Expr a)
instance Data.Hashable.Class.Hashable (Language.Elsa.Types.Expr a)
instance Language.Elsa.UX.PPrint (Language.Elsa.Types.Expr a)
instance GHC.Classes.Eq (Language.Elsa.Types.Bind a)
instance Language.Elsa.UX.PPrint (Language.Elsa.Types.Bind a)
instance Language.Elsa.UX.PPrint [Language.Elsa.Types.Bind a]

module Language.Elsa.Parser
parse :: FilePath -> Text -> SElsa
parseFile :: FilePath -> IO SElsa
instance Text.Megaparsec.Error.ShowErrorComponent Text.Megaparsec.Pos.SourcePos

module Language.Elsa.Eval
elsa :: Elsa a -> [Result a]
elsaOn :: (Id -> Bool) -> Elsa a -> [Result a]

module Language.Elsa.Runner
topMain :: IO ()
runElsa :: Mode -> FilePath -> Text -> IO ()
runElsaId :: FilePath -> Id -> IO (Maybe (Result ()))

module Language.Elsa