Module macros 

Macro system for defining reusable logical patterns

This module provides a powerful macro system that allows users to define parameterized logical patterns that can be reused throughout their expressions.

Syntax

Macros are defined using the following syntax:

DEFINE MACRO name(param1, param2, ...) = expression

Examples

// Define a transitive relation macro
DEFINE MACRO transitive(R, x, z) = EXISTS y. (R(x, y) AND R(y, z))

// Define a symmetric relation macro
DEFINE MACRO symmetric(R, x, y) = R(x, y) AND R(y, x)

// Define a reflexive relation macro
DEFINE MACRO reflexive(R, x) = R(x, x)

// Define an equivalence relation macro
DEFINE MACRO equivalence(R, x, y) = reflexive(R, x) AND reflexive(R, y) AND symmetric(R, x, y)

// Use macros in expressions
transitive(friend, Alice, Bob)

Structs

MacroDef

A macro definition with parameters and body

MacroRegistry

Registry for managing macro definitions

Functions

parse_macro_definition

Parse a macro definition from a string