OAI/Combinatorics/KMedian/Binary/BinaryListZip.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.Binary.ListZip.enc line 15
2. def OAI.MetricKMedian.Binary.ListZip.body line 17
3. def OAI.MetricKMedian.Binary.ListZip.result line 20
4. def OAI.MetricKMedian.Binary.ListZip.program line 21
5. theorem OAI.MetricKMedian.Binary.ListZip.run line 34
6. def OAI.MetricKMedian.Binary.ListZip.loop line 57
7. def OAI.MetricKMedian.Binary.PolyProgram.listZip line 68
8. def OAI.MetricKMedian.Binary.PolyProgram.listZipWith line 73