Kindelia/Kind2
1
1
Fork 0
mirror of https://github.com/Kindelia/Kind2.git synced 2024-09-17 10:59:12 +03:00
Code Issues Projects Releases Wiki Activity
2,232 Commits 10 Branches 10 Tags 56 MiB
f19e5c5546
Commit Graph

2232 Commits

This Branch
This Branch
All Branches
Author SHA1 Message Date
caotic123
f19e5c5546 Fix proofs after rigile modifications 2021-10-14 00:21:06 -03:00
caotic123
cca573698c Merge branch 'master' of https://github.com/uwu-tech/Kind 2021-10-13 23:33:36 -03:00
caotic123
4f40c9a8ce Move files and update on Bytes 2021-10-13 17:57:40 -03:00
rheidner
bad977011d Merge branch 'master' of https://github.com/uwu-tech/Kind 2021-10-13 14:18:25 -03:00
rheidner
69b0c5ff13 create tail version of bits.hex.encode 2021-10-13 14:13:26 -03:00
Rígille S. B. Menezes
38a8e049a4
Merge pull request #298 from rigille/master 
expand natural number lib
 2021-10-13 12:25:37 -03:00
Rígille S. B. Menezes
d4a38801de remove tiger 2021-10-13 12:23:43 -03:00
Rígille S. B. Menezes
1eee54b72e prove more theorems about natural numbers 2021-10-13 12:20:13 -03:00
Rígille S. B. Menezes
528db93c6c substitution looking good 2021-10-11 22:59:22 -03:00
Rígille S. B. Menezes
4527b483e9 prove commutativity of Nat.max 2021-10-11 19:21:49 -03:00
Rígille S. B. Menezes
832abfa665
Merge branch 'uwu-tech:master' into master 2021-10-11 14:37:20 -03:00
Rígille S. B. Menezes
b9a0defe16 create blueprint for decision procedure 2021-10-11 13:05:14 -03:00
Rígille S. B. Menezes
1368f8c6a7 remove more holes 2021-10-10 15:37:09 -03:00
Rígille S. B. Menezes
34eca25dd3 remove some more holes from addition theorems 2021-10-09 17:34:09 -03:00
Rígille S. B. Menezes
744a40557f fix Nat.mul proofs 2021-10-08 22:56:02 -03:00
Derenash
670a9cfe94 Fixed bugs in App/HotS 2021-10-07 22:14:41 -03:00
Rígille S. B. Menezes
2a6c57bf64 start removing all holes from theorem proofs 2021-10-07 18:19:49 -03:00
caotic123
e0f4634bb3 add proof of padding 2021-10-07 01:10:23 -03:00
caotic123
46d3e18988 add progress on proofs 2021-10-06 01:07:16 -03:00
Rígille S. B. Menezes
0ef4c5cedd
Merge branch 'uwu-tech:master' into master 2021-10-05 22:48:22 -03:00
MaiaVictor
b0513abc5e Remove Litereum files 2021-10-05 16:50:19 -03:00
MaiaVictor
5b50146480 Fixed and polishments 2021-10-05 16:44:59 -03:00
MaiaVictor
09d5fb1ec6 Remove unecessary check 2021-10-05 15:20:51 -03:00
MaiaVictor
703989fa3d Optimize serialization of local vars to use Bruijn indices 2021-10-05 15:13:07 -03:00
rheidner
2035f5c047 Lit: fix order of prints in example code 2021-10-05 13:37:04 -03:00
rheidner
b352081547 Merge branch 'master' of https://github.com/uwu-tech/Kind 2021-10-05 13:18:38 -03:00
rheidner
6b6ab1c1c3 Lit: show block correctly 2021-10-05 13:18:21 -03:00
Rígille S. B. Menezes
fd09f3c004 restore debian binary package files 2021-10-05 13:05:59 -03:00
Rígille S. B. Menezes
0c79bb4176 Merge branch 'master' of github.com:uwu-tech/Kind 2021-10-05 12:55:40 -03:00
Rígille S. B. Menezes
761be0168b add todos 2021-10-05 12:54:15 -03:00
rheidner
1826f4bea1 Lit: resolve 0 problem with varlen serialization 2021-10-05 11:03:13 -03:00
MaisaMilena
ec49dafd9d
Parse UTF-8 into String (#297) 
* Add some functions related to Bytes and others

* Add some byte functions and tests

* Add more bytes funcs and decode for utf-8 - needs to test

* Update some names in tests for bytes

* Update some test

* Update kind version on Playground

* Add some bytes funcs

* WIP with Bytes.to_string

* WIP Bytes.parse_string.aux grrr

* Can decode Bytes.test.parse_string.2

* Can parse some strings

* Most part of string parsing from UTF-8

* Clean some code and update tests in Bytes.test.all

* fix from victor version

* Remove Scheme target, add comment about WIP

Co-authored-by: caotic123 <camposferreiratiago@gmail.com>
 2021-10-04 23:15:58 -03:00
rheidner
0111bb8d2c Lit: verify at run if name is being redefined 2021-10-04 17:55:42 -03:00
rheidner
131484e8f6 Merge branch 'master' of https://github.com/uwu-tech/Kind 2021-10-04 15:04:57 -03:00
rheidner
58c9ae27c4 Lit: fix serialization 2021-10-04 15:04:51 -03:00
MaiaVictor
165d05c3eb Fix usage of the get syntax 2021-10-04 12:06:49 -03:00
MaiaVictor
bb13e74b1e Add serialization/deserialization test (not working yet) 2021-10-03 22:58:10 -03:00
MaiaVictor
df6dd3965d Litereum massive simplification DONE 2021-10-03 21:27:04 -03:00
MaiaVictor
a8f88e7080 Litereum massive simplification WIP 2021-10-03 17:33:09 -03:00
MaiaVictor
5e196909d9 Litereum massive simplification WIP 2021-10-03 15:16:33 -03:00
MaiaVictor
075d53a597 for-in loops can destruct lists of tuples 2021-10-03 13:37:14 -03:00
MaiaVictor
1dfcf525be Merge branch 'master' of github.com:uwu-tech/kind 2021-10-03 12:44:15 -03:00
MaiaVictor
a3e4912f19 Allow destructuring triples, quadruples, etc. with let 2021-10-03 12:43:39 -03:00
Rígille S. B. Menezes
f7afaea80d prove some inequalities 2021-10-02 13:53:50 -03:00
MaiaVictor
499a7ee369 Lit.Core partial refactor 2021-10-01 20:53:44 -03:00
MaiaVictor
f5e5a19405 Change caller stack from Maybe to List 2021-10-01 13:40:29 -03:00
MaiaVictor
5869bbdca8 Complete hole 2021-10-01 13:17:46 -03:00
MaiaVictor
3edc63a11f Improve readability 2021-10-01 13:17:07 -03:00
MaiaVictor
002c3c179d GPT3 changes 2021-10-01 13:03:42 -03:00
MaiaVictor
2007e78f5f Remove aux fn 2021-10-01 13:03:36 -03:00