summaryrefslogtreecommitdiff
path: root/Nominal/NameRestriction/Model.lean
AgeCommit message (Expand)Author
2026-01-12prove depth-0 axiomsHannes Schulze
2026-01-11prove some more axiomsHannes Schulze
2026-01-11prove well-definedness of restrict operationHannes Schulze
2026-01-10well-definedness of unionHannes Schulze
2026-01-10add model at depth 0Hannes Schulze