core

Documentation

Index

• func AlphaEq(a, b ast.Term) bool
• func Conv(a, b ast.Term, _ EtaFlags) bool
• 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(a, b ast.Term, _ EtaFlags) bool

Conv reports whether terms a and b are definitionally equal under the given eta flags. Strategy: normalize via NbE then alpha-compare normal forms. (We keep eta-expansion in eval.Reify for functions/pairs behind flags later; for now, Conv simply compares the normal forms returned by eval.Normalize.)

Types

type EtaFlags

type EtaFlags struct{ Pi, Sigma bool }