Danila Fedorin DanilaFe
0 Followers · 0 Following
Repositories
11
 Projects Packages Code Public Activity Starred Repositories
DanilaFe pushed to main at DanilaFe/agda-spa 2024-03-01 21:04:04 -08:00
ae09a27f64 Prove that finite value-maps are finite height
ca90f6509c Re-write the IterProd proofs to couple lattice and finite height lattice
29898e738b Clean up a bit
3a537f54ba Add a helpful utility function
52e7a7a208 Prove distributivity in the other direction, too
Compare 5 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-26 00:00:31 -08:00
8715d6d89c Finish proof of from distributivity
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-25 20:29:10 -08:00
b083561629 Add most of the proof of from distributivity.
3ad7db738a Prove that 'to' preserves equality
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-25 18:08:33 -08:00
53a08b8f79 Prove that 'first' presrves equality
d6064ff752 Expose 'locate' and 'forget' from Map
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-25 14:13:24 -08:00
d280f5afdf Make auxillary definitions private
b96bac5518 Prove the other direction for inverses.
99fc21cef2 Expose 'subset-impl' from Map
2a06e6ae2d Adjust 'to' to make it easier to reason about
Compare 4 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-19 22:58:11 -08:00
671ffc82df Define to-and-from functions from finite maps to tuples and prove one inverse direction
486b552b59 Try to generalize universe levels where possible
Compare 2 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-18 23:27:05 -08:00
aafcb2683d Prove the transport of 'height lattice' property given an isomorphism
8c9f39ac35 Add some additional 'equivalence' definitions to Equivalence
6384f7006e Make 'lattice' public
Compare 3 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-11 21:21:27 -08:00
b1c6b4c99a Expose bundles from Unit
5420bb808e Expose bundles from 'Prod'
4c0860f4c7 Expose bundle form MapSet
e89418d600 Expose bundle form 'Map'
bfb32092c2 Expose bundles and apply so renames to IterProd
Compare 9 commits »
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-11 15:39:47 -08:00
45f2babfa3 Fix typo in FixedHeightLattice definition
16c4d13242 Prove that iterated products are finite height
0ba4b46e16 Add proof of decidable equivalence for products
7e5cc1b316 Add an 'iterated product' lattice for A x A ... x A x B.
33b7bc37f0 Add a 'FiniteHeightLattice' bundle
Compare 11 commits »
DanilaFe pushed to master at DanilaFe/dotfiles 2024-02-10 14:33:52 -08:00
e6eb69e31b Merge remote-tracking branch 'origin/master'
4bf96b1296 Add more vim config changes
Compare 2 commits »
DanilaFe pushed to master at DanilaFe/dotfiles 2024-02-10 14:31:00 -08:00
3e6a62b798 Configure CLS and chplcheck
DanilaFe pushed to main at DanilaFe/agda-spa 2024-02-07 22:51:18 -08:00
a55c786a51 Tentatively start working on a language to analyze
DanilaFe pushed to master at Web-Projects/blog-static 2023-12-22 22:15:32 -08:00
16086e79b0 Proofread and publish bergamot post
b001bba3b8 Tweak rendering rules to support int(x) and str(x).
0c895a2662 Add an initial draft of the Bergamot post.
Compare 3 commits »
DanilaFe pushed to main at Everything-I-Know.../bergamot-elm 2023-12-22 21:59:56 -08:00
bc83f0ed53 Add bidirectional inference for int(?x) and str(?x).
DanilaFe pushed to master at Web-Projects/blog-static 2023-12-22 16:05:10 -08:00
6f0641f315 Render variables better
dc9dbe8a0f Update for bergamot requiring an 'input program' too
0b8096f973 Tweak the menu selector style
Compare 3 commits »
DanilaFe pushed to main at Everything-I-Know.../bergamot-elm 2023-12-22 16:00:20 -08:00
12d823e944 Configure prommpts via a Bergamot program, too.
DanilaFe pushed to main at Everything-I-Know.../bergamot-elm 2023-12-22 15:23:04 -08:00
9fd60b4013 Reorganize the UI somewhat and add conclusion-only view
aa7fd44a6d Slightly tweak code for proving a term
da470f5caa Add an occurss check to avoid infinite terms
Compare 3 commits »
DanilaFe pushed to master at Web-Projects/blog-static 2023-12-21 21:29:04 -08:00
d58a2a9975 Add overflow scroll to proof tree view.
DanilaFe pushed to master at Web-Projects/blog-static 2023-12-21 17:26:34 -08:00
a83268a6e3 Update use of the bergamot widget
DanilaFe pushed to main at Everything-I-Know.../bergamot-elm 2023-12-21 17:25:57 -08:00
abd6a848f8 Add support for editing the meta rules
535c714b47 Remove yields and switch to depth-based gas.
363e52ec5e Switch entirely to using rules to render rules.
84c79ddb50 Render sections in widget
678e51f146 Allow implicit sections to have more than one rule
Compare 7 commits »