defun-core

Defunctionalization helpers: core definitions.

The package defun provides defunctionalization helpers, most importantly type family DeFun.Core.App allowing to write higher-order type families. The singletons package also has its own type family Apply, but the machinery is tied to the Sing / singletons.

In particular, the Lam counterpart SLambda is specialized to Sing arguments. The defun's Lam is however fully general, so you can use your own singletons or (importantly) singleton-like arguments.

The package provides few defunctionalized functions, and their term-level variants can be found in defun-bool and defun-sop packages, which use SBool and NP data types from singletons-bool and sop-core packages respectively.