Danila Fedorin

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 »

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 »