senvas
0 followers · 0 following
  • Joined on 2024-02-15
Repositories
3
 Projects Packages Public activity Starred repositories
senvas pushed to main at senvas/ladder-calculus 2024-09-19 01:48:49 +02:00
dbfe0cf4de add initial impl of debruijn terms
826077e37b coq: add translate_typing example
d23ad61ba3 coq: type equiv: add subfun/submorph
6e5c832db7 add notation for sequence types & use notations everywhere
Compare 4 commits »
senvas pushed to main at senvas/ladder-calculus 2024-09-17 18:36:37 +02:00
633843d9c7 work on abstract & intro
127debf945 terms notation: add ident rule to allow variables in notation instance
f53f226f55 remove module wraps in each file
Compare 3 commits »
senvas pushed to main at senvas/ladder-calculus 2024-09-16 17:58:25 +02:00
05c137c489 import implementation of Fsub from the Coq tutorial of UPenn
senvas pushed to main at senvas/ladder-calculus 2024-09-16 17:54:54 +02:00
44d8d401d8 adapt eval relation & add reduction example
12da3e97bd change meaning of expr_ascend to only explicitly state the top segment of the type ladder.
cae0572e1b wip on preservation proof
Compare 3 commits »
senvas deleted branch master from senvas/ladder-calculus 2024-09-08 15:37:22 +02:00
senvas deleted branch wip from senvas/ladder-calculus 2024-09-08 15:37:19 +02:00
senvas created branch main in senvas/ladder-calculus 2024-09-08 15:36:24 +02:00
senvas pushed to main at senvas/ladder-calculus 2024-09-08 15:36:24 +02:00
638ddf4fd1 coq: add translate_typing
10ca08c5a0 coq typing relation: add DescendImplicit rule in addition to Descend rule for explicit type-downcasts
4b3358372e coq: typing relation fix ctx assignments in premisse
b44e443879 add translate_morphism_path \& morphism path examples
850285cff0 morphism paths: add Lift path
Compare 9 commits »
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 »