senvas
0 followers · 0 following
  • Joined on 2024-02-15
Repositories
3
 Projects Packages Public activity Starred repositories
senvas pushed to wip at senvas/ladder-calculus 2024-09-05 11:20:31 +02:00
6f81686105 paper: define morphism-path relation, redefine typing-relation \& translation
senvas pushed to wip at senvas/ladder-calculus 2024-09-04 13:01:32 +02:00
2d557e51e4 WIP coq: debruijn terms
d1742c51d5 coq: remove delta_step definition
1bd55cd8c3 paper: rename inference rules to match coq definitions
fd8ca35a27 paper: add new coq files to appendix
Compare 4 commits »
senvas pushed to wip at senvas/ladder-calculus 2024-09-04 12:41:29 +02:00
b31c8abc6c initial definition of soundness theorems
2db774ae68 initial definition of expand_morphisms
75fab989d7 work on typing rules
b978637b57 coq: change notation brackets for terms
719cb8ec4a coq: add value requirement in E-App2
Compare 5 commits »
senvas pushed to refactor2 at syntaxAlchemist/lib-nested 2024-09-02 00:14:11 +02:00
689ac95486 posint get_value() : ignore invalid digits
9b5dfc9cca posint example: switch between synced editors based on list of editor types
9f53b65074 tty backend: hooks to setup display for binary, octal, decimal \& hex notations of PosInt
4b7d929abc morphisms to copy edittree from <List Digit> to <PosInt ..>
38c772389f build repr tree
Compare 10 commits »
senvas pushed to refactor2 at syntaxAlchemist/lib-nested 2024-09-02 00:10:02 +02:00
ff80a0cba0 posint get_value() : ignore invalid digits
3ec8164202 posint example: switch between synced editors based on list of editor types
b9e73584c5 tty backend: hooks to setup display for binary, octal, decimal \& hex notations of PosInt
7268ed9bc9 morphisms to copy edittree from <List Digit> to <PosInt ..>
f60f8b2ac8 build repr tree
Compare 10 commits »
senvas pushed to refactor2 at syntaxAlchemist/lib-nested 2024-08-23 13:58:27 +02:00
2749e41fce add more types to detach
fb796cda04 add static TypeIDs to create basic types without context
Compare 2 commits »
senvas created branch refactor2 in syntaxAlchemist/lib-nested 2024-08-22 17:42:22 +02:00
senvas pushed to refactor2 at syntaxAlchemist/lib-nested 2024-08-22 17:42:22 +02:00
7226cb0162 add static TypeIDs to create basic types without context
e7331b36ae radix convert: accept radix=0 for native digit radix (2^64)
Compare 2 commits »
senvas pushed to wip at senvas/ladder-calculus 2024-08-22 09:05:26 +02:00
9c17e9e642 paper: rename inference rules to match coq definitions
senvas pushed to wip at senvas/ladder-calculus 2024-08-22 08:31:28 +02:00
4323e7d09f coq: add another typing example
ad107759bf coq: expr alpha conversion
39f312b401 coq: rename expr_term constructors: remove 'tm' prefix
Compare 3 commits »
senvas pushed to wip at senvas/ladder-calculus 2024-08-21 20:12:55 +02:00
b0035e711a wip
senvas pushed to wip at senvas/ladder-calculus 2024-08-21 19:58:13 +02:00
61f1234fcc coq: add 'compatible' typing relation
361d03c117 coq: reimplement type substitution and alpha conversion in types
0caf3ff514 coq: remove type_unit & type_num
Compare 3 commits »
senvas pushed to wip at senvas/ladder-calculus 2024-08-21 14:57:12 +02:00
42ae93f2d7 coq: add subtype relations
a65a33d9d6 coq: rename type equality rules to have prefix TEq_
d08144434c complete type distribute/condense definitions
221c017640 coq: alpha conversion in types
3a84dada65 coq notation definition for expressions
Compare 5 commits »
senvas deleted branch topic-parser from syntaxAlchemist/lt-core 2024-08-14 00:33:42 +02:00
senvas created branch topic-lib-structure in syntaxAlchemist/lt-core 2024-08-14 00:27:27 +02:00
senvas pushed to topic-lib-structure at syntaxAlchemist/lt-core 2024-08-14 00:27:27 +02:00
6c6f283352 diagnostic formatting: respect tab characters
184c8f3d50 separate crates for compiler-lib, compiler-cli and vm
Compare 2 commits »
senvas created branch master in senvas/handlebar-grip 2024-08-14 00:03:05 +02:00
senvas pushed to master at senvas/handlebar-grip 2024-08-14 00:03:05 +02:00
d4ad7cb4be initial commit
senvas created repository senvas/handlebar-grip 2024-08-13 20:03:19 +02:00
senvas pushed to topic-morphism-base at syntaxAlchemist/lib-laddertypes 2024-08-12 21:19:11 +02:00
5d7668573a initial implementation of solver for steiner trees