Commits · 9e71839a01017b75ecb80c70aae70e307e0fb662 · gradual-typing / sgdt · GitLab

Snippets Groups Projects

May 06, 2018
- [agda] start implementing renaming · 65a0b1c7
  Max New authored 6 years ago
  
  65a0b1c7
May 05, 2018
- [agda] change names, add upcast cells, need to add substitution · 877c0bfc
  Max New authored 6 years ago
  
  877c0bfc
- [agda] finish value transitivity well-formedness lemma · f946cae3
  Max New authored 6 years ago
  
  f946cae3
- [agda] rewrite with some agdaisms, think it will work now · b6caa730
  Max New authored 6 years ago
  
  b6caa730
May 03, 2018
- when an F meets a U · 294b2fcb
  Max New authored 6 years ago
  
  294b2fcb
Apr 28, 2018
- [agda] new version of composites, might work? · 53107377
  Max New authored 6 years ago
  
  53107377
Apr 27, 2018
- [agda] change to de bruijn because of better judgmental equality · ee37f2eb
  Max New authored 6 years ago
  
  ee37f2eb
Apr 26, 2018
- start doing the boundary calculuations, a lot of unexpectedly dumb obligations · ff89dff7
  Max New authored 6 years ago
  
  ff89dff7
- most of the multiplicative term lang, val transitivity was hard · 10178f61
  Max New authored 6 years ago
  
  10178f61
Apr 25, 2018
- Add computation transitivity, some sanity checking · 3d3f3e64
  Max New authored 6 years ago
  
  3d3f3e64
- start on agda, coq encodings of gcbpv, use dimension indices! · c2aae633
  Max New authored 6 years ago
  
  c2aae633