a Pure Type System Interpreter

Syntax

  expr ::= x, y, z
        | α, β, γ            (or \alpha, \beta, ...)
        | *, □ , △           (or [], /\)
        | ∀(x: expr). expr   (or Π,\Pi,\P,\forall)
        | expr → expr        (or ->)
        | λ(x: expr). expr   (or \,\l,\lambda)
        | expr expr
        | let x(: expr)? = expr in expr
						

System

STLC F Fω CoC HOL

λ* U- U Custom

S = {*; □ } A = {*: □ } R = {*, *, *}

Prettify Type Only Evaluate