git.iko.soy/Idris-dev
on master help sign in
fix image paths
b6fde49Martin Baker
docs/proofs/elabReflection.rst+5−5
compare with master
unifiedsplit
@@ -7,13 +7,13 @@ In order to extend the language we need to know something about how Idris is com
7
7
8Here is a diagram of the multistage process at the top level when Idris code gets compiled:
8Here is a diagram of the multistage process at the top level when Idris code gets compiled:
9
9
10−.. image:: image/idrisTopLevel.png
10+.. image:: ../image/idrisTopLevel.png
11 :width: 484px
11 :width: 484px
12 :height: 147px
12 :height: 147px
13
13
14TT 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.
14TT 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.
15
15
16−.. image:: image/compareToProofAssist.png
16+.. image:: ../image/compareToProofAssist.png
17 :width: 229px
17 :width: 229px
18 :height: 114px
18 :height: 114px
19
19
@@ -28,20 +28,20 @@ Type checker:
28- include universe levels
28- include universe levels
29- distinguish between global and local bound names.
29- distinguish between global and local bound names.
30
30
31−.. image:: image/elabOverview.png
31+.. image:: ../image/elabOverview.png
32 :width: 268px
32 :width: 268px
33 :height: 219px
33 :height: 219px
34
34
35As 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:
35As 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:
36
36
37−.. image:: image/binders.png
37+.. image:: ../image/binders.png
38 :width: 310px
38 :width: 310px
39 :height: 203px
39 :height: 203px
40
40
41.. list-table::
41.. list-table::
42
42
43 * - There is an elaborator for both definitions and terms, the definition elaborator calls the term elaborator when required.
43 * - 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
45 :width: 141px
45 :width: 141px
46 :height: 145px
46 :height: 145px
47
47
docs/proofs/example1.rst+8−8
@@ -23,7 +23,7 @@ Example 1
23 We fill that with 'intro' which creates a lambda term with a hole for the expression.
23 We fill that with 'intro' which creates a lambda term with a hole for the expression.
24 - diagram
24 - diagram
25
25
26− .. image:: image/tree.png
26+ .. image:: ../image/tree.png
27 :width: 133px
27 :width: 133px
28 :height: 106px
28 :height: 106px
29
29
@@ -44,14 +44,14 @@ After each tactic we will look at the state:
44 * - 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:
44 * - 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:
45 - state
45 - state
46
46
47− .. image:: image/elabProofStateEx1_1.png
47+ .. image:: ../image/elabProofStateEx1_1.png
48 :width: 310px
48 :width: 310px
49 :height: 124px
49 :height: 124px
50
50
51 * - We can also look at the logic at each stage:
51 * - We can also look at the logic at each stage:
52 - logic
52 - logic
53
53
54− .. image:: image/elabLogicEx1_1.png
54+ .. image:: ../image/elabLogicEx1_1.png
55 :width: 126px
55 :width: 126px
56 :height: 33px
56 :height: 33px
57
57
@@ -98,14 +98,14 @@ After each tactic we will look at the state:
98 * - state now looks like this
98 * - state now looks like this
99 - state
99 - state
100
100
101− .. image:: image/elabProofStateEx1_2.png
101+ .. image:: ../image/elabProofStateEx1_2.png
102 :width: 312px
102 :width: 312px
103 :height: 124px
103 :height: 124px
104
104
105 * - logic now looks like this
105 * - logic now looks like this
106 - logic
106 - logic
107
107
108− .. image:: image/elabLogicEx1_2.png
108+ .. image:: ../image/elabLogicEx1_2.png
109 :width: 126px
109 :width: 126px
110 :height: 45px
110 :height: 45px
111
111
@@ -152,14 +152,14 @@ After each tactic we will look at the state:
152 * - state now looks like this
152 * - state now looks like this
153 - state
153 - state
154
154
155− .. image:: image/elabProofStateEx1_3.png
155+ .. image:: ../image/elabProofStateEx1_3.png
156 :width: 312px
156 :width: 312px
157 :height: 124px
157 :height: 124px
158
158
159 * - logic now looks like this
159 * - logic now looks like this
160 - logic
160 - logic
161
161
162− .. image:: image/elabLogicEx1_3.png
162+ .. image:: ../image/elabLogicEx1_3.png
163 :width: 131px
163 :width: 131px
164 :height: 45px
164 :height: 45px
165
165
@@ -218,7 +218,7 @@ After each tactic we will look at the state:
218 * - logic now looks like this
218 * - logic now looks like this
219 - logic
219 - logic
220
220
221− .. image:: image/elabLogicEx1_4.png
221+ .. image:: ../image/elabLogicEx1_4.png
222 :width: 131px
222 :width: 131px
223 :height: 14px
223 :height: 14px
224
224
docs/proofs/tactics.rst+1−1
@@ -17,7 +17,7 @@ Tactics operate on the proof state. The proof state contains various pieces of i
17
17
18There 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.
18There 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.
19
19
20−.. image:: image/elabProofState.png
20+.. image:: ../image/elabProofState.png
21 :width: 283px
21 :width: 283px
22 :height: 232px
22 :height: 232px
23
23