- Portland, OR
- https://danilafe.com
- Joined on
2017-09-08
Block a user
53a08b8f79
Prove that 'first' presrves equality
d6064ff752
Expose 'locate' and 'forget' from Map
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
671ffc82df
Define to-and-from functions from finite maps to tuples and prove one inverse direction
486b552b59
Try to generalize universe levels where possible
aafcb2683d
Prove the transport of 'height lattice' property given an isomorphism
8c9f39ac35
Add some additional 'equivalence' definitions to Equivalence
6384f7006e
Make 'lattice' public
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
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
e6eb69e31b
Merge remote-tracking branch 'origin/master'
4bf96b1296
Add more vim config changes
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.
6f0641f315
Render variables better
dc9dbe8a0f
Update for bergamot requiring an 'input program' too
0b8096f973
Tweak the menu selector style
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
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
5c83f234c6
Include rendering rules in Bergamot widget.
24abec4045
Add some more CSS for the updates to the bergamot widget