leopold
0 Followers · 0 Following
  • Joined on 2023-09-12
Repositories
4
 Projects
1
 Packages Public Activity Starred Repositories
leopold pushed to main at leopold/inductive-verification-lean 2026-03-11 17:12:15 +01:00
e41142896f Proved basic properties of Blanchet protocol
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 13:20:59 +01:00
c705c80f23 Replaced some cases instances with grind
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 13:16:18 +01:00
70ab4d3c70 Replaced some cases instances with grind
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 13:12:37 +01:00
00542447b9 Replaced some cases instances with grind
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 12:59:27 +01:00
136780bfda Replaced some cases instances with grind
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 12:56:04 +01:00
b5328b520b Replaced some cases instances with grind
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 10:32:13 +01:00
7324a942d9 Replaced some cases instances with grind
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 10:13:05 +01:00
6299c20d71 Replaced some cases instances with grind
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 10:05:32 +01:00
943525dfb5 Replaced some cases instances with grind
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 10:02:53 +01:00
4e97dd4028 Replaced some cases instances with grind
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 02:30:03 +01:00
80db88efbe Added expand_parts_element macro
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 02:05:14 +01:00
58c093b18d Added expand_parts_element macro
leopold pushed to main at leopold/inductive-verification-lean 2026-03-05 00:45:27 +01:00
4732515f78 Added expand_parts_element macro
leopold pushed to main at leopold/inductive-verification-lean 2026-03-04 19:12:31 +01:00
2c84c4a975 Added expand_parts_element macro
leopold pushed to main at leopold/inductive-verification-lean 2026-03-04 18:44:53 +01:00
0f017b08b5 Added expand_parts_element macro
leopold pushed to main at leopold/inductive-verification-lean 2026-03-04 00:57:05 +01:00
7367681bc6 Simplified proofs in NS_Public
leopold pushed to main at leopold/inductive-verification-lean 2026-02-25 17:27:36 +01:00
96e5d59603 Finished proff of NS
leopold pushed to main at leopold/inductive-verification-lean 2026-02-23 09:06:47 +01:00
31e638dd90 Translated library, started to prove NS_Public
leopold pushed to main at leopold/songsheet_generator 2025-02-13 17:11:03 +01:00
c468ec7d57 added python app
leopold pushed to main at leopold/songsheet_generator 2025-02-08 16:54:07 +01:00
96273071bb added offertory verses to propers: