MdHighlightCode.md 1.3 KB

MdHighlightCode

  • Avdol
    • Yes!
    • I!
    • Am!
  • Jojo!

Jojo! This is the last of my hamon! Take it from me!!

Everything above should be preserved

module Kira where
data KillerQueue

-- this code should be preserved

module MdHighlightCode where

open import Agda.Builtin.Nat

This is an Agda code block ↑

number : Nat
number = suc (suc zero)
This is an Agda code block as well ↑