thorin::Check Class Reference

#include <thorin/check.h>

Public Member Functions
	Check (World &world)
World &	world ()

Static Public Member Functions
template<bool infer = true>
static bool	alpha (Ref d1, Ref d2)
	Are d1 and d2 α-equivalent?
static bool	assignable (Ref type, Ref value)
	Can value be assigned to sth of type?
static Ref	is_uniform (Defs defs)
	Yields defs.front(), if all defs are Check::alpha-equivalent (infer = false) and nullptr otherwise.

Detailed Description

Definition at line 47 of file check.h.

Constructor & Destructor Documentation

Check()

thorin::Check::Check ( World &  world )

inline

Definition at line 49 of file check.h.

Member Function Documentation

alpha()

template<bool infer = true>

static bool thorin::Check::alpha ( Ref  d1, Ref  d2  )

inlinestatic

Are d1 and d2 α-equivalent?

• In infer mode, type inference is happening and Infers will be resolved, if possible. Also, two free but different Vars are considered α-equivalent.
• When **not* in infer mode, no type inference is happening and Infers will not be touched. Also, Two free but different Vars are not considered α-equivalent.

Definition at line 59 of file check.h.

References thorin::Infer::Check, and thorin::Def::world().

Referenced by thorin::Pi::check(), thorin::Lam::check(), thorin::Arr::check(), thorin::World::extract(), thorin::World::insert(), and thorin::World::test().

assignable()

static bool thorin::Check::assignable ( Ref  type, Ref  value  )

inlinestatic

Can value be assigned to sth of type?

Note

This is different from equiv(type, value->type()) since type may be dependent.

Definition at line 63 of file check.h.

References thorin::Infer::Check, thorin::Def::type(), and thorin::Def::world().

Referenced by thorin::World::app(), thorin::Lam::check(), thorin::World::iapp(), thorin::World::insert(), and thorin::World::tuple().

is_uniform()

Ref thorin::Check::is_uniform ( Defs  defs )

static

Yields defs.front(), if all defs are Check::alpha-equivalent (infer = false) and nullptr otherwise.

Definition at line 213 of file check.cpp.

Referenced by thorin::World::sigma(), and thorin::World::tuple().

world()

World & thorin::Check::world ( )

inline

Definition at line 52 of file check.h.

---

The documentation for this class was generated from the following files:

• include/thorin/check.h
• src/thorin/check.cpp