Back to NPA

Declaration

Vec

Mathlib.Vector.Basic

Packages

2

Module

63

Theorems

750

Declarations

1016

Untrusted sidecar

Source text and display overlays are presentation metadata. The signed certificate and checker result are the trusted evidence.

Statement

Type

Proof term

inductive Vec : Type where | unit : Vec