diff options
| author | JJ | 2024-07-15 19:28:30 +0000 |
|---|---|---|
| committer | JJ | 2024-07-15 20:48:34 +0000 |
| commit | a5a6418813900441e846e6853711dff94d1f9406 (patch) | |
| tree | 30230e3015d3c0339c8d9d83c786150696617265 /untyped | |
| parent | 060acee3310597b5ddbd9bf42635d8ebbdef8f34 (diff) | |
backport interpret-/infer-/check- renaming and remove implicit params
Diffstat (limited to 'untyped')
0 files changed, 0 insertions, 0 deletions