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-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 »
DanilaFe pushed to master at Nix-Configs/server-config 2023-12-16 11:35:14 -08:00
2286867025 Pin the blog nixpkgs to the OS nixpkgs.
DanilaFe pushed to master at Nix-Configs/katex-html 2023-12-16 10:22:53 -08:00
9ddfb114c7 Adjust the KaTeX script to skip rendering in <script> tags
DanilaFe pushed to master at Web-Projects/blog-static 2023-12-03 00:03:27 -08:00
5c83f234c6 Include rendering rules in Bergamot widget.
24abec4045 Add some more CSS for the updates to the bergamot widget
Compare 2 commits »
DanilaFe pushed to main at Everything-I-Know.../bergamot-elm 2023-12-02 23:55:04 -08:00
18d524a0d2 Avoid checking for out-of-gas on each 'andThen'
d6d610c038 Save the current rules I'm using for rendering LaTeX.
11dd5ee9fd Put render rules separately from regular rules
1d3f3fd3f8 Use 'lazy' to speed up re-rendering
f964a60412 Perform metavariable substitution from quoting
Compare 23 commits »
DanilaFe pushed to master at Nix-Configs/server-config 2023-11-29 23:43:59 -08:00
ea0a65fd34 Update flake.lock to even later working version of packages