senvas
0 followers · 0 following
  • Joined on 2024-02-15
Repositories
3
 Projects Packages Public activity Starred repositories
senvas pushed to topic-morphism-base at syntaxAlchemist/lib-laddertypes 2024-08-05 02:55:00 +02:00
811adde1b9 turn Morphism into trait and add find_morphism() function
senvas created branch topic-semantic-subtype in syntaxAlchemist/lib-laddertypes 2024-08-05 00:12:12 +02:00
senvas pushed to topic-semantic-subtype at syntaxAlchemist/lib-laddertypes 2024-08-05 00:12:12 +02:00
3b85bd7621 add find_semantic_subtype_matches() as potential alternative to is_semantic_subtype_of()
senvas pushed to topic-morphism-base at syntaxAlchemist/lib-laddertypes 2024-08-05 00:11:46 +02:00
42286bcadc add test for find_morphism_path()
b835cddcf1 initial MorphismBase with DFS to find morphism paths
486760f3e2 TypeID: add Copy trait
a4837038e6 Merge branch 'topic-parameter-normal-form' into dev
Compare 4 commits »
senvas pushed to dev at syntaxAlchemist/lib-laddertypes 2024-08-05 00:11:21 +02:00
a4837038e6 Merge branch 'topic-parameter-normal-form' into dev
senvas pushed to topic-morphism-base at syntaxAlchemist/lib-laddertypes 2024-08-05 00:10:54 +02:00
b127c9eb79 add test for find_morphism_path()
48c12d9d18 initial MorphismBase with DFS to find morphism paths
ca65e152bc TypeID: add Copy trait
886598aeb3 Merge branch 'topic-parameter-normal-form' into dev
02d8815acd add param_normalize() to get Parameter-Normal-Form (PNF)
Compare 5 commits »
senvas pushed to dev at syntaxAlchemist/lib-laddertypes 2024-08-05 00:10:19 +02:00
886598aeb3 Merge branch 'topic-parameter-normal-form' into dev
02d8815acd add param_normalize() to get Parameter-Normal-Form (PNF)
Compare 2 commits »
senvas pushed to topic-morphism-base at syntaxAlchemist/lib-laddertypes 2024-08-04 23:57:23 +02:00
a52f38dadf add test for find_morphism_path()
f09ee8c7c0 initial MorphismBase with DFS to find morphism paths
a75a7a56a0 TypeID: add Copy trait
658134d56a readme: add syntax description and roadmap
Compare 4 commits »
senvas pushed to topic-morphism-base at syntaxAlchemist/lib-laddertypes 2024-08-04 23:48:06 +02:00
6a5c27cfba add test for find_morphism_path()
senvas created branch topic-morphism-base in syntaxAlchemist/lib-laddertypes 2024-08-04 23:28:05 +02:00
senvas pushed to topic-morphism-base at syntaxAlchemist/lib-laddertypes 2024-08-04 23:28:05 +02:00
64b9d98a1f initial MorphismBase with DFS to find morphism paths
fcd58baec6 TypeID: add Copy trait
Compare 2 commits »
senvas pushed to refactor at syntaxAlchemist/lib-nested 2024-08-03 15:44:15 +02:00
4c0e9da2d3 fixup examples
senvas pushed to refactor at syntaxAlchemist/lib-nested 2024-08-02 22:43:29 +02:00
830ce613ea example: two editors with different radices
a3c701ce88 automatically generate list-map morphisms in find_morphism()
Compare 2 commits »
senvas pushed to refactor at syntaxAlchemist/lib-nested 2024-08-01 18:36:27 +02:00
6e8bb0aeb5 apply_list_map_morphism
senvas pushed to dev at Fragmental/light-control 2024-07-31 21:13:43 +02:00
eb42f5fa54 full hue range in arctic rain
17de5bcb76 show average fps on console
f8148462d2 update pastel fade
Compare 3 commits »
senvas pushed to master at senvas/ladder-calculus 2024-07-27 13:30:56 +02:00
c7794d8a89 paper: wip add more lemmas
eebb096f8a coq: wip typing
d880e07d57 coq: notations for type terms
Compare 3 commits »
senvas pushed to master at senvas/ladder-calculus 2024-07-25 12:43:05 +02:00
13165a7951 coq: smallstep: define delta expansion
ec955c3c19 coq: add morphism type
292234c247 rename term types to expr_term and type_term and type_abs->type_univ, type_app->type_spec
Compare 3 commits »
senvas pushed to master at senvas/ladder-calculus 2024-07-25 11:05:29 +02:00
f2a5d4a11b rename term types to expr_term and type_term and type_abs->type_univ, type_app->type_spec
senvas created branch master in senvas/ladder-calculus 2024-07-24 11:25:26 +02:00
senvas pushed to master at senvas/ladder-calculus 2024-07-24 11:25:26 +02:00
ec1a2ab4a4 add initial main.tex
84ad8d9897 coq: add some examples of bb-encoding
04f9393b4f coq: preliminary small-step semantics
d8200b56b4 coq: preliminary definition of typing-relation
a6939b3a40 coq: equivalence of type-terms