b6fde49 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

fix image paths

commitb6fde49227ad6bfd56aa1ec259380d8db4f7e9a4 authorMartin Baker <git87465@martinb.com> dateWed 8 May 2019, 16:44 (7 years ago) parentcd58dfb

3 files changed+14−14

compare with master

unifiedsplit

docs/proofs/elabReflection.rst+5−5 docs/proofs/example1.rst+8−8 docs/proofs/tactics.rst+1−1

docs/proofs/elabReflection.rst+5−5

@@ -7,13 +7,13 @@ In order to extend the language we need to know something about how Idris is com

88Here is a diagram of the multistage process at the top level when Idris code gets compiled:

10−.. image:: image/idrisTopLevel.png

10+.. image:: ../image/idrisTopLevel.png

1111 :width: 484px

1212 :height: 147px

1313

1414TT is a core language which is syntactically very simple, this makes it easy for computers to process but very verbose and hard for humans to read. This elaboration is done by a logic language (proof tactics) similar to LTac in Coq. Here we use the word 'tactics' to refer to these elaboration tactics - not to be confused with the old tactics mechanism.

1515

16−.. image:: image/compareToProofAssist.png

16+.. image:: ../image/compareToProofAssist.png

1717 :width: 229px

1818 :height: 114px

1919

@@ -28,20 +28,20 @@ Type checker:

2828- include universe levels

2929- distinguish between global and local bound names.

3030

31−.. image:: image/elabOverview.png

31+.. image:: ../image/elabOverview.png

3232 :width: 268px

3333 :height: 219px

3434

3535As already mentioned the TT core language is kept syntactically very simple. Part of the reason for this is that its correctness is already well proven using logic. For instance, here are the binders in TT with corresponding code and logic type introduction rules:

3636

37−.. image:: image/binders.png

37+.. image:: ../image/binders.png

3838 :width: 310px

3939 :height: 203px

4040

4141.. list-table::

4242

4343 * - There is an elaborator for both definitions and terms, the definition elaborator calls the term elaborator when required.

44− - .. image:: image/elab.png

44+ - .. image:: ../image/elab.png

4545 :width: 141px

4646 :height: 145px

4747

docs/proofs/example1.rst+8−8

@@ -23,7 +23,7 @@ Example 1

2323 We fill that with 'intro' which creates a lambda term with a hole for the expression.

2424 - diagram

2525

26− .. image:: image/tree.png

26+ .. image:: ../image/tree.png

2727 :width: 133px

2828 :height: 106px

2929

@@ -44,14 +44,14 @@ After each tactic we will look at the state:

4444 * - In order to investigate how the program works we can look at the proofState at each stage as the tactics are applied. So here is the proofState at the start:

4545 - state

4646

47− .. image:: image/elabProofStateEx1_1.png

47+ .. image:: ../image/elabProofStateEx1_1.png

4848 :width: 310px

4949 :height: 124px

5050

5151 * - We can also look at the logic at each stage:

5252 - logic

5353

54− .. image:: image/elabLogicEx1_1.png

54+ .. image:: ../image/elabLogicEx1_1.png

5555 :width: 126px

5656 :height: 33px

5757

@@ -98,14 +98,14 @@ After each tactic we will look at the state:

9898 * - state now looks like this

9999 - state

100100

101− .. image:: image/elabProofStateEx1_2.png

101+ .. image:: ../image/elabProofStateEx1_2.png

102102 :width: 312px

103103 :height: 124px

104104

105105 * - logic now looks like this

106106 - logic

107107

108− .. image:: image/elabLogicEx1_2.png

108+ .. image:: ../image/elabLogicEx1_2.png

109109 :width: 126px

110110 :height: 45px

111111

@@ -152,14 +152,14 @@ After each tactic we will look at the state:

152152 * - state now looks like this

153153 - state

154154

155− .. image:: image/elabProofStateEx1_3.png

155+ .. image:: ../image/elabProofStateEx1_3.png

156156 :width: 312px

157157 :height: 124px

158158

159159 * - logic now looks like this

160160 - logic

161161

162− .. image:: image/elabLogicEx1_3.png

162+ .. image:: ../image/elabLogicEx1_3.png

163163 :width: 131px

164164 :height: 45px

165165

@@ -218,7 +218,7 @@ After each tactic we will look at the state:

218218 * - logic now looks like this

219219 - logic

220220

221− .. image:: image/elabLogicEx1_4.png

221+ .. image:: ../image/elabLogicEx1_4.png

222222 :width: 131px

223223 :height: 14px

224224

docs/proofs/tactics.rst+1−1

@@ -17,7 +17,7 @@ Tactics operate on the proof state. The proof state contains various pieces of i

1717

1818There are many other pieces of information in the proof state such as the names used , such as the bodies of case blocks that need to be elaborated.but, for now, we will leave the system to handle these.

1919

20−.. image:: image/elabProofState.png

20+.. image:: ../image/elabProofState.png

2121 :width: 283px

2222 :height: 232px

2323