Elaboratorial This is the accompanying code for tutorials on elaboration. Tutorial 1: Bidirectional Elaboration for the Simply-Typed Lambda Calculus youtube link