#!/usr/bin/env bash
# Typecheck the Cassini-identity proof and print its axiom footprint.
# Exit 0 with no error lines = QED (the kernel accepted the proof).
set -euo pipefail
export PATH="$HOME/.elan/bin:$PATH"
HERE="$(cd "$(dirname "$0")" && pwd)"
command -v lean >/dev/null 2>&1 || { echo "Lean not found — run install-lean.sh first." >&2; exit 127; }
echo "Lean: $(lean --version)"
echo "Typechecking Cassini.lean …"
lean "$HERE/Cassini.lean"
echo "✓ typechecks (no errors above)."
echo
echo "Axiom footprint (must be [propext] or [propext, Quot.sound], NO sorryAx, NO Classical.choice):"
lean "$HERE/Cassini.lean" 2>&1 | grep -i "depends on axioms\|does not depend" || true