core

Documentation

Index

• func AlphaEq(a, b ast.Term) bool
• func Conv(env *Env, t, u ast.Term, opts ConvOptions) bool
• func ConvLegacy(a, b ast.Term, flags EtaFlags) bool
• type ConvOptions
• type Env
  • func NewEnv() *Env
  • func (e *Env) Extend(t ast.Term) *Env
• type EtaFlags

Functions

func AlphaEq

func AlphaEq(a, b ast.Term) bool

AlphaEq compares two core terms modulo alpha (de Bruijn makes this structural).

func Conv

func Conv(env *Env, t, u ast.Term, opts ConvOptions) bool

Conv reports whether t and u are definitionally equal under env. If opts.EnableEta is true, use η-rules for functions (Pi) and pairs (Sigma).

Implementation strategy: 1. Evaluate both terms to Values using NbE 2. Reify both Values back to normal forms 3. Apply η-expansion if enabled 4. Compare normal forms structurally

func ConvLegacy

func ConvLegacy(a, b ast.Term, flags EtaFlags) bool

Conv (legacy) - wrapper for backward compatibility

Types

type ConvOptions

type ConvOptions struct {
	EnableEta bool // Enable η-equality for functions (Π) and pairs (Σ)
}

ConvOptions controls the behavior of definitional equality checking.

type Env

type Env struct {
	// contains filtered or unexported fields
}

Env represents a typing environment for conversion checking. For now, this is a simple wrapper around eval.Env.

func NewEnv

func NewEnv() *Env

NewEnv creates a new empty environment.

func (*Env) Extend

func (e *Env) Extend(t ast.Term) *Env

Extend adds a term to the environment by evaluating it.

type EtaFlags

type EtaFlags struct{ Pi, Sigma bool }

Legacy API compatibility - kept for existing tests