Danila Fedorin

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

DanilaFe pushed to master at Nix-Configs/blog-static-flake

2023-11-29 23:36:14 -08:00

f704ceda8d Update web-files version which has newer bergamot.

DanilaFe pushed to master at Nix-Configs/web-files

2023-11-29 23:35:24 -08:00

50fdf4b452 Update bergamot version

DanilaFe pushed to master at Web-Projects/blog-static

2023-11-29 23:26:19 -08:00

56ff56281e Add missing SCSS file for bergamot.