lam.h File Reference

#include <variant>
#include "mim/def.h"

Include dependency graph for lam.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	mim::Pi
	A dependent function type. More...
class	mim::Lam
	A function. More...
class	mim::App

Namespaces
namespace	mim

Typedefs
Lam
GIDSet / GIDMap keyed by Lam::gid of Lam*.
template<class To >
using	mim::LamMap = GIDMap<Lam*, To>
using	mim::LamSet = GIDSet<Lam*>
using	mim::Lam2Lam = LamMap<Lam*>

Functions
Helpers to work with Functions
const App *	mim::isa_callee (const Def *def, size_t i)
Lam *	mim::isa_workable (Lam *lam)
	These are Lams that are neither nullptr, nor Lam::is_external, nor Lam::is_unset.
std::pair< const App *, Lam * >	mim::isa_apped_mut_lam (const Def *def)
std::deque< const App * >	mim::decurry (const Def *)
	Yields curried Apps in a flat std::deque<const App*>.
const Def *	mim::compose_cn (const Def *f, const Def *g)
	The high level view is:
std::pair< const Def *, std::vector< const Def * > >	mim::collect_args (const Def *def)
	Helper function to cope with the fact that normalizers take all arguments and not only its axiom arguments.