Certified Agda statements

Data.Nat.Properties.+-comm

Algebra.Definitions.Commutative{⟨0⟩}{⟨0⟩}{ℕ}(Agda.Builtin.Equality._≡_{⟨0⟩}{ℕ})Agda.Builtin.Nat._+_Algebra.Definitions.Commutativelevellmax0HRWCxlevellmax0HRWCxAgda.Builtin.Nat.NatHRWCxAgda.Builtin.Equality._≡_levellmax0HRWCxAgda.Builtin.Nat.NatHRWCxVRWCxAgda.Builtin.Nat._+_VRWCx

Display: Presentation MathML from an uncertified display map. Certified: the LaTeX text and the Content MathML.

Certified LaTeX

\mathsf{Algebra.Definitions.Commutative} \{ \langle 0 \rangle \} \{ \langle 0 \rangle \} \{ \mathbb{N} \} \, ( \mathsf{Agda.Builtin.Equality.\_≡\_} \{ \langle 0 \rangle \} \{ \mathbb{N} \} ) \, \mathsf{Agda.Builtin.Nat.\_+\_}

certificate sha256 be6cdf29def511a8f55f0fcc2a346bc7663117e948532c55cca706f2cc1d7989 · table tbl0-stdlib sha256 1b8317f1120a43683e2732aadff3605b269357565f47bad57324ff18cf811790 · Agda 2.8.0 · elision off · display: unfolded (anonymous-module aliases unfolded and leading hidden binders exposed; definitionally the declared type)

Verified for this page: stock Agda 2.8.0 accepted CertMain, CertBind and 4 probe programs (--safe); every literal bound; core e2c48291f26148d4; theorem source src/Data/Nat/Properties.agda sha256 6d2b3ebf95ea18af

What these certificates do not claim