<commit_before># System T

This is an implementation of the language __T__ from
[PFPL](http://www.cs.cmu.edu/~rwh/pfpl.html). It uses the CMU ABT library (the
one used in the [15-312 course](https://www.cs.cmu.edu/~rwh/courses/ppl/) at CMU).

The aim is to closely follow the description in PFPL. All typing rules can be
found in `src/statics/typechecker.sml` and all dynamics rules in
`src/dynamics/dynamics.sml` somewhere close to the corresponding lines of code.

## Building

You need `smlnj` to build along with `ml-lex` and `ml-yacc`. Given that you have
these installed, just `make` in the project directory. If all goes well you
should find an executable `bin/repl`. Here is an example repl session:

```
> (\(x:nat) s(x))(s(s(z)))
Step: s(s(s(z)))
s(s(s(z))) : nat
> rec s(s(s(z))) {z => z | s(u) with v => s(s(s(v)))}
Step: s(s(s(rec(z; x@7.x@8.s(s(s(x@8))); s(s(z))))))
Step: s(s(s(s(s(s(rec(z; x@11.x@12.s(s(s(x@12))); s(z))))))))
Step: s(s(s(s(s(s(s(s(s(rec(z; x@15.x@16.s(s(s(x@16))); z))))))))))
Step: s(s(s(s(s(s(s(s(s(z)))))))))
s(s(s(s(s(s(s(s(s(z))))))))) : nat
```

Note that instead of ↪ we use =>.<commit_msg>Added another example in README<commit_after># System T

This is an implementation of the language __T__ from
[PFPL](http://www.cs.cmu.edu/~rwh/pfpl.html). It uses the CMU ABT library (the
one used in the [15-312 course](https://www.cs.cmu.edu/~rwh/courses/ppl/) at CMU).

The aim is to closely follow the description in PFPL. All typing rules can be
found in `src/statics/typechecker.sml` and all dynamics rules in
`src/dynamics/dynamics.sml` somewhere close to the corresponding lines of code.

## Building

You need `smlnj` to build along with `ml-lex` and `ml-yacc`. Given that you have
these installed, just `make` in the project directory. If all goes well you
should find an executable `bin/repl`. Here is an example repl session:

```
> (\(x:nat) s(x))(s(s(z)))
Step: s(s(s(z)))
s(s(s(z))) : nat
> \ (x:nat) s(s(x))
lam{nat}(x@2.s(s(x@2))) : arr(nat; nat)
> rec s(s(s(z))) {z => z | s(u) with v => s(s(s(v)))}
Step: s(s(s(rec(z; x@7.x@8.s(s(s(x@8))); s(s(z))))))
Step: s(s(s(s(s(s(rec(z; x@11.x@12.s(s(s(x@12))); s(z))))))))
Step: s(s(s(s(s(s(s(s(s(rec(z; x@15.x@16.s(s(s(x@16))); z))))))))))
Step: s(s(s(s(s(s(s(s(s(z)))))))))
s(s(s(s(s(s(s(s(s(z))))))))) : nat
```

Note that instead of ↪ we use =>.
{'fraction_non_alphanumeric': 0.23162393162393163, 'fraction_numerical': 0.017948717948717947, 'mean_word_length': 4.80893300248139, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 14, 'https://': 2, 'lorem ipsum': 0, 'www.': 4, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '5053043', 'n_tokens_mistral': 1063, 'n_tokens_neox': 1020, 'n_words': 281}