subst

Documentation

Index

• func IShift(d, cutoff int, t ast.Term) ast.Term
• func IShiftFace(d, cutoff int, f ast.Face) ast.Face
• func ISubst(j int, s ast.Term, t ast.Term) ast.Term
• func ISubstFace(j int, s ast.Term, f ast.Face) ast.Face
• func Shift(d, cutoff int, t ast.Term) ast.Term
• func ShiftFace(d, cutoff int, f ast.Face) ast.Face
• func Subst(j int, s ast.Term, t ast.Term) ast.Term
• func SubstFace(j int, s ast.Term, f ast.Face) ast.Face

Functions

func IShift

func IShift(d, cutoff int, t ast.Term) ast.Term

IShift shifts all free interval variables >= cutoff by d positions. This operates in the interval variable namespace, separate from term variables.

func IShiftFace

func IShiftFace(d, cutoff int, f ast.Face) ast.Face

IShiftFace shifts interval variables in a face formula.

func ISubst

func ISubst(j int, s ast.Term, t ast.Term) ast.Term

ISubst substitutes interval term s for interval variable j in t. This operates in the interval variable namespace.

func ISubstFace

func ISubstFace(j int, s ast.Term, f ast.Face) ast.Face

ISubstFace substitutes an interval term for an interval variable in a face formula.

func Shift

func Shift(d, cutoff int, t ast.Term) ast.Term

Shift shifts all free de Bruijn variables >= cutoff by d positions. Follows TAPL §6.2.1.

func ShiftFace

func ShiftFace(d, cutoff int, f ast.Face) ast.Face

ShiftFace shifts term variables in a face formula (faces have no term vars).

func Subst

func Subst(j int, s ast.Term, t ast.Term) ast.Term

Subst substitutes s for variable j in t, adjusting indices. Follows TAPL §6.2.2.

func SubstFace

func SubstFace(j int, s ast.Term, f ast.Face) ast.Face

SubstFace substitutes a term for a term variable in a face formula.