summaryrefslogtreecommitdiff
path: root/Nominal/NameRestriction/Model.lean
AgeCommit message (Collapse)Author
2026-01-13add M_1 model structureHannes Schulze
2026-01-12prove well-definedness of absHannes Schulze
2026-01-12cleanupHannes Schulze
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