changeset | fe231950824a |
---|---|
branch | default |
bookmark | |
tag | tip |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Define not in SystemT |
files | systemF.agda |
changeset | ca278492b95f |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Try Redefine R. but not proof lemma-R-n |
files | systemF.agda |
changeset | 42027b9a70ef |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Add some lemma for Prodcut |
files | int.agda systemF.agda |
changeset | dcc57765bdef |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Fix R arguments for check speed up |
files | int.agda |
changeset | 02926d953ef7 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Retry define add-r. use R twice |
files | int.agda |
changeset | 7b0f2025112b |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Define Add on Int |
files | int.agda systemF.agda |
changeset | 852798763d56 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Tree |
files | systemF.agda |
changeset | 2efb882e120d |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Define Binary Tree |
files | systemF.agda |
changeset | 36d0732d28e5 |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Add comment for lemma-list-nil-cons |
files | systemF.agda |
changeset | 46fce75667cb |
---|---|
branch | |
bookmark | |
tag | |
user | Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp> |
description | Retry prove lemma-list-nil-cons. but not finished. |
files | systemF.agda |