Danila Fedorin DanilaFe
0 Sekotāji · 0 Seko
Repozitoriji
11
 Projekti Pakotnes Kods Publiskā aktivitāte Atzīmēti repozitoriji
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-03-04 01:38:29 +00:00
164fc3636f Prove that constant functions are monotonic
c932210d37 Re-expert monotonicity from Lattice
a8d26b1c48 Prove that join is monotonic in both arguments
2ddac38c3f Update with new changes to Agda
Salīdzināt 4 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-03-03 00:24:14 +00:00
f00dabfc93 More cleanup to FiniteValueMap
01f4e02026 More cleanup to FiniteValueMap
fbbcd72037 Some early refactors of FiniteValueMap
03cdc65a7b Format AboveBelow a bit better (round two)
ec2b1ec3ba Format FiniteMap a little bit better
Salīdzināt 7 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-03-02 07:46:27 +00:00
6cb6281bc2 Make main run the fixed point algorithm
0774946211 Expose decidability from Map modules
65d1590358 Prove monotonicity of lub in one argument
ae3e2c28b0 Create bundles and add a program to evaluate some code with finite maps
97a4165b58 Expose bundles from FiniteValueMap
Salīdzināt 5 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-03-02 05:14:52 +00:00
754714d770 Restore bundles in IterProd
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-03-02 05:04:04 +00: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
Salīdzināt 5 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-02-26 08:00:31 +00:00
8715d6d89c Finish proof of from distributivity
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-02-26 04:29:10 +00:00
b083561629 Add most of the proof of from distributivity.
3ad7db738a Prove that 'to' preserves equality
Salīdzināt 2 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-02-26 02:08:33 +00:00
53a08b8f79 Prove that 'first' presrves equality
d6064ff752 Expose 'locate' and 'forget' from Map
Salīdzināt 2 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-02-25 22:13:24 +00: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
Salīdzināt 4 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-02-20 06:58:11 +00: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
Salīdzināt 2 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-02-19 07:27:05 +00:00
aafcb2683d Prove the transport of 'height lattice' property given an isomorphism
8c9f39ac35 Add some additional 'equivalence' definitions to Equivalence
6384f7006e Make 'lattice' public
Salīdzināt 3 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-02-12 05:21:27 +00: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
Salīdzināt 9 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-02-11 23:39:47 +00: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
Salīdzināt 11 revīzijas »
DanilaFe iesūtīja izmaiņas master repozitorijā DanilaFe/dotfiles 2024-02-10 22:33:52 +00:00
e6eb69e31b Merge remote-tracking branch 'origin/master'
4bf96b1296 Add more vim config changes
Salīdzināt 2 revīzijas »
DanilaFe iesūtīja izmaiņas master repozitorijā DanilaFe/dotfiles 2024-02-10 22:31:00 +00:00
3e6a62b798 Configure CLS and chplcheck
DanilaFe iesūtīja izmaiņas main repozitorijā DanilaFe/agda-spa 2024-02-08 06:51:18 +00:00
a55c786a51 Tentatively start working on a language to analyze
DanilaFe iesūtīja izmaiņas master repozitorijā Web-Projects/blog-static 2023-12-23 06:15:32 +00: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.
Salīdzināt 3 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā Everything-I-Know…/bergamot-elm 2023-12-23 05:59:56 +00:00
bc83f0ed53 Add bidirectional inference for int(?x) and str(?x).
DanilaFe iesūtīja izmaiņas master repozitorijā Web-Projects/blog-static 2023-12-23 00:05:10 +00:00
6f0641f315 Render variables better
dc9dbe8a0f Update for bergamot requiring an 'input program' too
0b8096f973 Tweak the menu selector style
Salīdzināt 3 revīzijas »
DanilaFe iesūtīja izmaiņas main repozitorijā Everything-I-Know…/bergamot-elm 2023-12-23 00:00:20 +00:00
12d823e944 Configure prommpts via a Bergamot program, too.