module Core.Context import public Core.Name -- Definition ------------------------------------------------------------------ public export data Context : Type where Lin : Context (:<) : Context -> Name -> Context %name Context sx, sy, sz