msullivan

with
  # I made an object Input with a data property, which made it easier to
  # develop this in the CLI. It also works fine to make the input a parameter.
  input := (select Input filter .day = 1).data,
  # input := <str>$0,
  grps := array_unpack(str_split(input[:-1], '\n\n')),
  sums := (for grp in grps union (
    with entries := <int64>array_unpack(str_split(grp, '\n')),
    select sum(entries)
  )),

msullivan

%%%% Formalization of a simply typed lambda-calculus with n-ary tuples.

% I decided to do this because it seemed like something small and
% interesting that was definitely not on the twelf wiki as a case
% study or a tutorial. n-ary tuples are a great feature in that they
% add no expressive power over pairs but are a much bigger pain to
% machine formalize!
%
% Doing it on paper is mostly just a matter of sprinkling "subscript i"
% and "..." around, but is otherwise pretty straightforward.