Module nar::check::pats

Patterns.

Modules

block	Reduction blocking status
core
mat	Match patterns.

Structs

Blocked

Something where a meta variable may block reduction. Agda.

Enums

Match	If matching is inconclusive (Dunno) we want to know whether it is due to a particular meta variable.
Simpl	Simplification in Agda.
Stuck	A modified version of this thing in Agda.

Functions

build_subst	Agda.
match_copats

Type Definitions

CoreCopat
CorePat
RedM	Reduce Monad.