MdHighlightCode.lagda.md 433 B

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 ↑