function application to get terms by choosing an argument and then a function with domain containing this.

function application to get terms by choosing a function and then a term in its domain

nodes combining backward reasoning targeting types that are (dependent) function types, aggregated over all types

nodes combining backward reasoning targeting types that are (dependent) function types, with domain product, sigma-types or co-products aggregated over all types

node for targeting functions on products by currying, and also on sigma-types and co-products

Node for folding a function (or term) with a speficied number of arguments to get terms.

Node for folding a function (or term) with a speficied target type to optionally get terms with the target type.

Node for fully folding a type family to get types

Node for generating terms of a type (if possible) by multiple applications of functions tageting the type.

Start of an indexed introduction rule by fully applying a type family

Extending indexed introduction rule by an iterated function ending in the inductive type family fully applied.

Aggregating extending indexed introduction rule by iterated function type eding in fully applied inductive type family.

Aggregating extending introduction types for indexed inductive types by iterated function types

Extending an indexed introduction rule by a specific unrelated type

aggregating extending introduction types for indexed inductive types by unrelated types

Aggregating extending indexed introduction rule by fully applied inductive type family.

Node for recursive definitions given an inductive definition, generating a domain and invoking the node getting codomain and recursion data

aggregated induction functions from inductive types

Inductive definitions from a given inductive definition by generating a domain and invoking the node getting codomain and recursion data

Recursive definition given an inductive definition and a domain, i.e., recursion function with data of the right type folded in.

induction function for a specific structure, picking the type family

extending types of iterated functions targeting W by the type typ

aggregating extensions of iterated function types

extension of the introduction rule for an inductive type W by a type of the form eg A -> W

node to generate partial applications of f from partial applications that are functions.

nodes combining lambdas with given domain that are (dependent) function types, aggregated over all domains

An island to generate lambda terms, i.e., terms are generated withing the island and exported as lambdas; the initial state of the island has a new variable mixed in.

lambda island for generating function with specified domain

node combining lambda islands aggregated by type

An island to generate lambda terms that are type families, i.e., terms are generated withing the island and exported as lambdas; the initial state of the island has a new variable mixed in.

node combining lambda islands targeting type families aggregated by type

A node for targeting a (dependent function) type, with variable of the domain generated and the co-domain type (more generally fibre) targeted within the island.

extensions of the introduction rule types for an inductive type W by an unrelated type C; we may have a Pi-Type with domain C rather than a FuncTyp there is no assumption on how the head type typ is generated, so this is reusable if only that is changed.

aggregating extensions of inductive types by unrelated types

single function application to generate partial applications of f, if f is a function

island to generate Pi-Types by taking variables with specified domain, similar to lambdaIsle

aggregate generation of Pi-types from islands

Node for recursive definitions picking an inductive definition, generating a domain and invoking the node getting codomain and recursion data

aggregate recursion functions from inductive types

Recursive definitions from a given inductive definition by generating a domain and invoking the node getting codomain and recursion data

Recursive definition given an inductive definition and a domain, i.e., recursion function with data of the right type folded in.

extend an introduction rule type for an inductive type W by W -> ...

island to generate Sigma-Types by taking variables with specified domain, similar to lambdaIsle

aggregate generation of Sigma-types from islands

builds an inductive definition, i.e.

builds an inductive structure from a bunch of introduction rules for a type inductiveTyp, we must separately specify how to build an introduction rules, as well as a vector of these.

Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here meant to be used for backward reasoning.

Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain and recursion data

Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here

Family of nodes for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here

terms generated by first choosing type and then term with the type; a form of backward reasoning

function application to get terms by choosing a type family and then a term in its domain, but without conditioning

function application to get types by choosing a type family and then a term in its domain, but without conditioning

Node for generating terms of a type (if possible) by multiple applications of functions targeting the type.

function application to get type families by choosing a type family and then a term in its domain, but without conditioning

function application with unification starting with type families, with output conditioned to be a type family.

Node family for fully folding type families to get types

types from a type family by filtering partial applications to consider only types.

function application with unification starting with type families, but with output not conditioned.

function application with unification starting with type families, with output conditioned to be a type.

function application with unification node to get terms

Wrapper for application to allow equality and toString to work.

Wrapper for flipped application to allow equality and toString to work.

Wrapper for lambda island to allow equality and toString to work.

Wrapper for lambda island tageting type families to allow equality and toString to work.

Wrapper for unified application to allow equality and toString to work.