OAI/Combinatorics/KMedianRecovery/Machines/RecoveryOptionMachine.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.replaceState line 10
2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.replaceState_computes line 12
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atOption line 18
4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atOption_computes line 20
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.replaceState_pack line 26
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atOption_none line 31
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atOption_some line 38