Module functions 

Auto-generated module

🤖 Generated with SplitRS

Functions

app

Build a left-associative application chain: f a1 a2 ....

app1

Build f a (single-argument application).

arrow

Build a non-dependent Pi type: A → B.

lam

Build a lambda: λ x → body.

pi

Build a dependent Pi type: (x : A) → B.

var

Build AgdaExpr::Var.