Commits · master · Raphaël Cauderlier / dklib

24 Jan, 2017 3 commits
- Github does not respect :noexport: · 35d5437d
  Raphael Cauderlier authored Jan 24, 2017
  
  35d5437d
- Add a README · 4ec7f1b8
  Raphael Cauderlier authored Jan 24, 2017
  
  4ec7f1b8
- [confluence] Require the path to CSI^HO instead of using locate. · 7fd665e4
  Raphael Cauderlier authored Jan 24, 2017
```
By default, no confluence checking, even if CSI^HO is installed
```
  7fd665e4
26 Aug, 2015 10 commits
- Don't check for confluence files depending on dk_binary_nat · 93e3fde4
  Raphaël Cauderlier authored Aug 26, 2015
  
  93e3fde4
- [dk_binary_nat] fix ordering by making them ortogonal · 099eea7a
  Raphaël Cauderlier authored Aug 26, 2015
  
  099eea7a
- Remove dk_binary_nat.length: This was nonsense since 0 = S0 0 have no finite length · 273e31f5
  Raphaël Cauderlier authored Aug 26, 2015
  
  273e31f5
- Fix an error in the definition of dk_binary_nat.mult · 398522c6
  Raphaël Cauderlier authored Aug 26, 2015
  
  398522c6
- Don't check dk_int for confluence (checker's answer is MAYBE) · c8138f22
  Raphaël Cauderlier authored Aug 26, 2015
  
  c8138f22
- Merge branch 'v2.4' of https://github.com/rafoo/dklib into v2.4 · f705f9f5
  Raphaël Cauderlier authored Aug 26, 2015
  
  f705f9f5
- [slist] New implementation, hopefully confluent · af8d2489
  Raphaël Cauderlier authored Aug 26, 2015
  
  af8d2489
- Symmetric addition is needed for confluence of dk_int.leq. · b4299305
  Raphaël Cauderlier authored Aug 26, 2015
  
  b4299305
- Renaming forgotten in dk_char · 67acc3ad
  Raphaël Cauderlier authored Aug 26, 2015
  
  67acc3ad
- Typo · d9af73ac
  Raphaël Cauderlier authored Aug 26, 2015
  
  d9af73ac
20 Aug, 2015 4 commits
- [Slist] Make insert_aux confluent. min is still not confluent. · 5fe6b6dd
  Raphaël Cauderlier authored Aug 20, 2015
  
  5fe6b6dd
- Move casting function between machine and binary numbers to · 081460d5
  Raphaël Cauderlier authored Aug 20, 2015
```
dk_binary_nat because it is hard to prove confluent and dk_binary_nat is
not checked for confluence.
```
  081460d5
- Add automatic checking of confluence. · 56e2d0ee
  Raphaël Cauderlier authored Aug 20, 2015
```
Comment hard to check rules and fix a confluence bug in dk_machine_int.
```
  56e2d0ee
- Rewrite rules on external symbols now work! (Thank you Ronan!). · 1ec3632f
  Raphaël Cauderlier authored Aug 20, 2015
```
Move rules on cc.eT to better locations so that cc.dk only talk about
dependent product and arrow.
```
  1ec3632f
19 Aug, 2015 4 commits
- Try using rewrite rule on cc.eT in a file different from cc (does not · b3340880
  Raphaël Cauderlier authored Aug 19, 2015
```
yet work)
```
  b3340880
- Fix inclusion of .depend files · ce755964
  Raphaël Cauderlier authored Aug 19, 2015
  
  ce755964
- Adapt all files to new Dedukti syntax · 2ba0577f
  Raphaël Cauderlier authored Aug 19, 2015
  
  2ba0577f
- Ronan's modification for syntax of Dedukti v2.4 · 68ef4834
  Raphaël Cauderlier authored Aug 19, 2015
  
  68ef4834
16 Feb, 2015 2 commits
- Remove unused checking options · 99a504fe
  Raphaël Cauderlier authored Feb 16, 2015
  
  99a504fe
- Correct slist · edebfd5f
  Raphaël Cauderlier authored Feb 16, 2015
  
  edebfd5f
22 Jan, 2015 2 commits
- [slist] Remove wildcard patterns; they are not supported by dkcheck any more. · 316b0161
  Raphaël Cauderlier authored Jan 22, 2015
  
  316b0161
- Makefile using new dkdep syntax allowing to break the correspondance · e2c49426
  Raphaël Cauderlier authored Jan 22, 2015
```
between .dk and .dko file names
```
  e2c49426
06 Oct, 2014 2 commits
- Add a file on sorted lists of natural numbers · 1ebfb416
  Raphaël Cauderlier authored Oct 06, 2014
  
  1ebfb416
- Inductive definition of dk_nat.min is more usable for inductive proofs. · dfeed096
  Raphaël Cauderlier authored Oct 06, 2014
  
  dfeed096
04 Jun, 2014 1 commit
- Avoid using underscores · 597c3be2
  Raphaël Cauderlier authored Jun 04, 2014
  
  597c3be2
20 Mar, 2014 2 commits
- Remove old file about object · bb1810cb
  Raphaël Cauderlier authored Mar 20, 2014
  
  bb1810cb
- Back to dedukti v2.2c · 086c37bc
  Raphaël Cauderlier authored Mar 20, 2014
  
  086c37bc
10 Mar, 2014 2 commits
- Update to Dedukti version 2.2.1 new syntax · 50dd5f09
  Raphaël Cauderlier authored Mar 10, 2014
  
  50dd5f09
- Move dk_obj to its own repo. · 639a0ea7
  Raphaël Cauderlier authored Mar 10, 2014
  
  639a0ea7
17 Feb, 2014 3 commits
- Uniformisation: use capital letters for types and lower letters for · 1a940969
  Raphaël Cauderlier authored Feb 17, 2014
```
terms in cc.uT
```
  1a940969
- [build] use wildcard to list source files · 5a70c71b
  Raphaël Cauderlier authored Feb 17, 2014
  
  5a70c71b
- Avoid type : e type. · a1cd06d2
  Raphaël Cauderlier authored Feb 17, 2014
  
  a1cd06d2
14 Feb, 2014 3 commits
- Remove istrue and bool · a479ff62
  Raphaël Cauderlier authored Feb 14, 2014
  
  a479ff62
- Add a point example · 3366643e
  Raphaël Cauderlier authored Feb 14, 2014
  
  3366643e
- Reverse the order of arguments of Ot_assoc · 73d62c45
  Raphaël Cauderlier authored Feb 14, 2014
  
  73d62c45
13 Feb, 2014 2 commits
- Monomorphisation of ifs · b59a17ed
  Raphaël Cauderlier authored Feb 13, 2014
  
  b59a17ed
- Remove the symbols method and methods which where abbreviation for Expr · 5062f481
  Raphaël Cauderlier authored Feb 13, 2014
```
-> Expr
```
  5062f481