Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
Copyright (c) 2022 Alex Keizer. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alex Keizer

import Lean

  Adds a `TypeVec` simp attribute.
  Has to be in a separate file from `TypeVec.lean`, since simp attributes cannot be used directly in
  the file that declares them.

/-- simp set for the manipulation of typevec and arrow expressions -/
register_simp_attr typevec