The Debug Page

1. Introduction

Hello, this is the debug page. I am trying to include one of each annoying thing.

2. Supported markdown

One of each of the things that I claim to support.

2.1. Standard markdown

This is a paragraph.

This is a blockquote. It should support multiline stuff
This is another paragraph within the blockquote. -- A.A. Milne

This paragraph has strong and emphasised elements in it. Here is a link to a really important website

I think that the above is a thematic break?

Now it's time to make some code examples:

(1)

def hello (x : String) : String :=
  -- this is some lean-ish code

Now

(2)

function this(asdf : Prop) {
    // is javascript woah.
}

2.2. Headers do support `inline` items, even $\frac{x}{y + 2}$ crazy maths.

2.2.1. Some less common markdowns.

Inline math block

(3)

\int_{0}^{\frac{π}{4}} (tan x)^{\frac{1}{3}} d x = = \int_{0}^{1} \frac{t ^{\frac{1}{3}}}{1 + t ^{2}} d t \int_{0}^{1} \frac{y}{1 + y ^{3}} d y

3. My markdown variant

Since I work in ITP, there are lots of abbreviations. ITP is the main one that I keep coming back to. If you hover over the abbreviations it should tell you what it stands for.

3.1. Captions

You can have sidenotes nowJust like this!.

3.2. References

You should be able to reference other sections, for example here I reference Section 3.1, Section 2.

3.2.1. Blockquote captions

We should be able to make captions appear for blockquotes:

Quotation 4

This is a cool caption that you can put your stuff in.

Note that captions can have multiple paragraphs and these should not render lame.

Hello world This is a quote that is captioned. I hope that you like it. Best wishes, Ed

You can caption anything which can be referenced like a figure. But note that the captions will get bunched up and might become misaligned with their source. I've resigned to not fix this.

(5)

This is a really important piece of maths

d (ln (\frac{cos ( a - x )}{cos ( x )})) = \frac{sin ( a )}{cos ( x ) cos ( a - x )} d x

The equation (5) should be referenced. [todo] this currently fails!