Ermine.Builtin.Term

Description

Synopsis

• lam :: Eq v => Binder v [Pattern t] -> Term t v -> Term t v
• dataCon :: Fixity -> String -> String -> Type Void Void -> Term t v
• let_ :: Eq v => Binder v [Binding t v] -> Term t v -> Term t v
• implicit :: [PreBody t v] -> PreBinding t v
• explicit :: t -> [PreBody t v] -> PreBinding t v
• bindings :: Eq v => [(v, PreBinding t v)] -> Binder v [Binding t v]
• data PreBinding t v = PreBinding Rendering (BindingType t) [PreBody t v]
• finalizeBindings :: Eq v => Binder v [PreBinding t v] -> [Binding t v]
• finalizeBinding :: Eq v => [v] -> PreBinding t v -> Binding t v
• data PreBody t v = PreBody (Binder v [Pattern t]) (Guarded (Term t v)) (Binder v [Binding t v])
• body :: Binder v [Pattern t] -> Term t v -> Binder v [Binding t v] -> PreBody t v
• gbody :: Binder v [Pattern t] -> [(Term t v, Term t v)] -> Binder v [Binding t v] -> PreBody t v
• shapely :: [PreBody t v] -> Bool
• finalizeBody :: Eq v => [v] -> PreBody t v -> Body t v

Documentation