Nov 23, 1-2 AM (5)
Nov 23, 2-3 AM (5)
Nov 23, 3-4 AM (7)
Nov 23, 4-5 AM (15)
Nov 23, 5-6 AM (8)
Nov 23, 6-7 AM (24)
Nov 23, 7-8 AM (27)
Nov 23, 8-9 AM (44)
Nov 23, 9-10 AM (16)
Nov 23, 10-11 AM (88)
Nov 23, 11-12 PM (21)
Nov 23, 12-1 PM (59)
Nov 23, 1-2 PM (45)
Nov 23, 2-3 PM (27)
Nov 23, 3-4 PM (42)
Nov 23, 4-5 PM (118)
Nov 23, 5-6 PM (23)
Nov 23, 6-7 PM (23)
Nov 23, 7-8 PM (19)
Nov 23, 8-9 PM (14)
Nov 23, 9-10 PM (15)
Nov 23, 10-11 PM (13)
Nov 23, 11-12 AM (4)
Nov 24, 12-1 AM (6)
Nov 24, 1-2 AM (8)
Nov 24, 2-3 AM (11)
Nov 24, 3-4 AM (8)
Nov 24, 4-5 AM (4)
Nov 24, 5-6 AM (11)
Nov 24, 6-7 AM (28)
Nov 24, 7-8 AM (18)
Nov 24, 8-9 AM (32)
Nov 24, 9-10 AM (24)
Nov 24, 10-11 AM (15)
Nov 24, 11-12 PM (36)
Nov 24, 12-1 PM (21)
Nov 24, 1-2 PM (9)
Nov 24, 2-3 PM (39)
Nov 24, 3-4 PM (36)
Nov 24, 4-5 PM (33)
Nov 24, 5-6 PM (8)
Nov 24, 6-7 PM (16)
Nov 24, 7-8 PM (24)
Nov 24, 8-9 PM (15)
Nov 24, 9-10 PM (10)
Nov 24, 10-11 PM (9)
Nov 24, 11-12 AM (8)
Nov 25, 12-1 AM (8)
Nov 25, 1-2 AM (9)
Nov 25, 2-3 AM (5)
Nov 25, 3-4 AM (5)
Nov 25, 4-5 AM (6)
Nov 25, 5-6 AM (8)
Nov 25, 6-7 AM (6)
Nov 25, 7-8 AM (9)
Nov 25, 8-9 AM (21)
Nov 25, 9-10 AM (89)
Nov 25, 10-11 AM (23)
Nov 25, 11-12 PM (25)
Nov 25, 12-1 PM (63)
Nov 25, 1-2 PM (84)
Nov 25, 2-3 PM (22)
Nov 25, 3-4 PM (16)
Nov 25, 4-5 PM (13)
Nov 25, 5-6 PM (7)
Nov 25, 6-7 PM (9)
Nov 25, 7-8 PM (10)
Nov 25, 8-9 PM (46)
Nov 25, 9-10 PM (23)
Nov 25, 10-11 PM (5)
Nov 25, 11-12 AM (8)
Nov 26, 12-1 AM (5)
Nov 26, 1-2 AM (1)
Nov 26, 2-3 AM (2)
Nov 26, 3-4 AM (3)
Nov 26, 4-5 AM (3)
Nov 26, 5-6 AM (13)
Nov 26, 6-7 AM (26)
Nov 26, 7-8 AM (29)
Nov 26, 8-9 AM (19)
Nov 26, 9-10 AM (21)
Nov 26, 10-11 AM (25)
Nov 26, 11-12 PM (16)
Nov 26, 12-1 PM (17)
Nov 26, 1-2 PM (27)
Nov 26, 2-3 PM (12)
Nov 26, 3-4 PM (22)
Nov 26, 4-5 PM (66)
Nov 26, 5-6 PM (10)
Nov 26, 6-7 PM (7)
Nov 26, 7-8 PM (13)
Nov 26, 8-9 PM (8)
Nov 26, 9-10 PM (3)
Nov 26, 10-11 PM (3)
Nov 26, 11-12 AM (1)
Nov 27, 12-1 AM (3)
Nov 27, 1-2 AM (1)
Nov 27, 2-3 AM (5)
Nov 27, 3-4 AM (2)
Nov 27, 4-5 AM (2)
Nov 27, 5-6 AM (1)
Nov 27, 6-7 AM (3)
Nov 27, 7-8 AM (1)
Nov 27, 8-9 AM (3)
Nov 27, 9-10 AM (3)
Nov 27, 10-11 AM (19)
Nov 27, 11-12 PM (13)
Nov 27, 12-1 PM (15)
Nov 27, 1-2 PM (1)
Nov 27, 2-3 PM (5)
Nov 27, 3-4 PM (3)
Nov 27, 4-5 PM (3)
Nov 27, 5-6 PM (3)
Nov 27, 6-7 PM (3)
Nov 27, 7-8 PM (1)
Nov 27, 8-9 PM (0)
Nov 27, 9-10 PM (2)
Nov 27, 10-11 PM (4)
Nov 27, 11-12 AM (2)
Nov 28, 12-1 AM (5)
Nov 28, 1-2 AM (3)
Nov 28, 2-3 AM (2)
Nov 28, 3-4 AM (5)
Nov 28, 4-5 AM (1)
Nov 28, 5-6 AM (1)
Nov 28, 6-7 AM (1)
Nov 28, 7-8 AM (1)
Nov 28, 8-9 AM (2)
Nov 28, 9-10 AM (3)
Nov 28, 10-11 AM (3)
Nov 28, 11-12 PM (2)
Nov 28, 12-1 PM (3)
Nov 28, 1-2 PM (5)
Nov 28, 2-3 PM (2)
Nov 28, 3-4 PM (9)
Nov 28, 4-5 PM (2)
Nov 28, 5-6 PM (2)
Nov 28, 6-7 PM (2)
Nov 28, 7-8 PM (3)
Nov 28, 8-9 PM (10)
Nov 28, 9-10 PM (26)
Nov 28, 10-11 PM (7)
Nov 28, 11-12 AM (5)
Nov 29, 12-1 AM (4)
Nov 29, 1-2 AM (9)
Nov 29, 2-3 AM (18)
Nov 29, 3-4 AM (21)
Nov 29, 4-5 AM (1)
Nov 29, 5-6 AM (6)
Nov 29, 6-7 AM (6)
Nov 29, 7-8 AM (16)
Nov 29, 8-9 AM (23)
Nov 29, 9-10 AM (37)
Nov 29, 10-11 AM (22)
Nov 29, 11-12 PM (25)
Nov 29, 12-1 PM (34)
Nov 29, 1-2 PM (32)
Nov 29, 2-3 PM (44)
Nov 29, 3-4 PM (25)
Nov 29, 4-5 PM (11)
Nov 29, 5-6 PM (16)
Nov 29, 6-7 PM (21)
Nov 29, 7-8 PM (47)
Nov 29, 8-9 PM (20)
Nov 29, 9-10 PM (11)
Nov 29, 10-11 PM (10)
Nov 29, 11-12 AM (7)
Nov 30, 12-1 AM (3)
Nov 30, 1-2 AM (0)
2,632 commits this week Nov 23, 2021 - Nov 30, 2021
SCP-3031 (#4211)
This PR modifies the syntax of algorithmic terms to make them easier to reason about.

The idea is to abstract over return types that contain functions: unwrap, type application and builtin.

Not doing this caused big problems later in values, builtin applications and evaluation contexts.

The pay off is to reduce the number of postulated lemmas, duplicated definitions, and extensions required.