Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- lamAbs0 ∷ t ~ Term DeBruijn uni fun () ⇒ t → t
- idFun0 ∷ Term DeBruijn uni fun ()
- const0 ∷ Term DeBruijn uni fun ()
- deepFun0 ∷ Natural → Term DeBruijn DefaultUni DefaultFun ()
- deeperFun0 ∷ Natural → Term DeBruijn DefaultUni DefaultFun ()
Documentation
lamAbs0 ∷ t ~ Term DeBruijn uni fun () ⇒ t → t Source #
A helper to intro the only "sensical" lam: debruijn binders are always 0-indexed
deepFun0 ∷ Natural → Term DeBruijn DefaultUni DefaultFun () Source #
(lam0 ...n.... (Var n)) Correct binders, well-scoped variable
deeperFun0 ∷ Natural → Term DeBruijn DefaultUni DefaultFun () Source #
(lam0 ...n.... lam0 ...n.... (Var n+n)) Correct binders, well-scoped variable