Mercurial > hg > Papers > 2013 > kono-prosym

annotate Agda.mm @ 0:aa359e82dab7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prosym paper 2013
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 28 Nov 2013 09:27:34 +0900
parents
children 888cc58ced9d
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 <map version="0.9.0">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 <!-- To view this file, download free mind mapping software FreeMind from http://freemind.sourceforge.net -->
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 <node CREATED="1384158495265" ID="ID_1057489819" MODIFIED="1384158505062" TEXT="Agda">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 <node CREATED="1384158505773" ID="ID_375459405" MODIFIED="1384158511281" POSITION="right" TEXT="Programming in Agda">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 <node CREATED="1384158511282" ID="ID_173554271" MODIFIED="1384158517612" TEXT="Programming?">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 <node CREATED="1384158518929" ID="ID_132864750" MODIFIED="1384158520292" TEXT="append"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 <node CREATED="1385553167504" ID="ID_655374031" MODIFIED="1385553174525" TEXT="normalzation as eval"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 <node CREATED="1385553140807" ID="ID_1697810219" MODIFIED="1385553143740" TEXT="Proof">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 <node CREATED="1385553144895" ID="ID_5020353" MODIFIED="1385553161258" TEXT="complain nothing is the goal"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 <node CREATED="1384158575905" ID="ID_1857200497" MODIFIED="1384158578202" POSITION="right" TEXT="Proof">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 <node CREATED="1384158578203" ID="ID_1658338767" MODIFIED="1384158586181" TEXT="Curry Howard"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 <node CREATED="1384158587810" ID="ID_1975721703" MODIFIED="1384158597800" TEXT="Lambda as proof"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 <node CREATED="1385554013320" ID="ID_1356905670" MODIFIED="1385554017783" TEXT="Martin Lof">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 <node CREATED="1385554020817" ID="ID_356163234" MODIFIED="1385554031250" TEXT="Intutionistic Logic"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 <node CREATED="1385552512024" ID="ID_147799666" MODIFIED="1385552516341" POSITION="right" TEXT="Agda Proof System">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 <node CREATED="1385552516856" ID="ID_1464159621" MODIFIED="1385552528505" TEXT="expression"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 <node CREATED="1385552559432" ID="ID_133092931" MODIFIED="1385552561277" TEXT="binding"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 <node CREATED="1385553356789" ID="ID_1762984421" MODIFIED="1385553364891" TEXT="implicit parameters"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 <node CREATED="1385552549038" ID="ID_1258388375" MODIFIED="1385552552692" TEXT="lambda expression"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 <node CREATED="1385552529036" ID="ID_1881312508" MODIFIED="1385552530633" TEXT="type"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 <node CREATED="1385552532612" ID="ID_40469366" MODIFIED="1385552535010" TEXT="equality">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 <node CREATED="1385597173078" ID="ID_503695732" MODIFIED="1385597179382" TEXT="relation"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28 <node CREATED="1385597180159" ID="ID_366226932" MODIFIED="1385597182662" TEXT="identity"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 <node CREATED="1385552538773" ID="ID_594724672" MODIFIED="1385552539866" TEXT="data">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 <node CREATED="1385552575615" ID="ID_1970582835" MODIFIED="1385552578092" TEXT="equality"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 <node CREATED="1385552540357" ID="ID_27933366" MODIFIED="1385552542986" TEXT="record"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 <node CREATED="1385553086985" ID="ID_1287863407" MODIFIED="1385553091444" TEXT="level of Set">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 <node CREATED="1385553107280" ID="ID_1726309329" MODIFIED="1385553114125" TEXT="especialy in set"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 <node CREATED="1385554049111" ID="ID_1268043793" MODIFIED="1385554060412" TEXT="Qunatifiers">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38 <node CREATED="1385554060934" ID="ID_98595305" MODIFIED="1385554062564" TEXT="for all"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
39 <node CREATED="1385554063438" ID="ID_938488241" MODIFIED="1385554066022" TEXT="exisits"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
41 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 <node CREATED="1385553423068" ID="ID_1167992721" MODIFIED="1385553433515" POSITION="right" TEXT="Comparing Haskell"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 <node CREATED="1384158640697" ID="ID_1899173298" MODIFIED="1384158643661" POSITION="right" TEXT="Category">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
44 <node CREATED="1385552494294" ID="ID_1015253891" MODIFIED="1385552505083" TEXT="definition of Category">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 <node CREATED="1385597141136" ID="ID_193939883" MODIFIED="1385597144786" TEXT="Monoid"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
47 <node CREATED="1384158643993" ID="ID_1820912347" MODIFIED="1384158649133" TEXT="natural transformation">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
48 <node CREATED="1385553771910" ID="ID_179921992" MODIFIED="1385553774629" TEXT="nkf example"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
49 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
50 <node CREATED="1385552884093" ID="ID_1465613770" MODIFIED="1385552886994" TEXT="What for?"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
52 <node CREATED="1385552342991" ID="ID_1939991054" MODIFIED="1385552354178" POSITION="left" TEXT="Proof by human">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
53 <node CREATED="1385552354669" ID="ID_154501585" MODIFIED="1385552370256" TEXT="wrote at book space"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54 <node CREATED="1385552371251" ID="ID_836715929" MODIFIED="1385552382002" TEXT="typed text"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
55 <node CREATED="1385552385336" ID="ID_1562417181" MODIFIED="1385552400070" TEXT="Written in Proof System"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
56 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 <node CREATED="1384158653521" ID="ID_666651656" MODIFIED="1384158659565" POSITION="left" TEXT="technique">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
58 <node CREATED="1384158660337" ID="ID_1951403393" MODIFIED="1384158666022" TEXT="?">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59 <node CREATED="1385553875993" ID="ID_1969521083" MODIFIED="1385553887280" TEXT="show type of this place"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
60 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 <node CREATED="1384158666649" ID="ID_1339522289" MODIFIED="1385552771364" TEXT="equaltion transformation">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62 <node CREATED="1385552998803" ID="ID_406773110" MODIFIED="1385553004592" TEXT="using ? in transformation"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63 <node CREATED="1385553932043" ID="ID_115305994" MODIFIED="1385553943751" TEXT="determine the result"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 <node CREATED="1385553955708" ID="ID_105082961" MODIFIED="1385553960578" TEXT="try and error">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 <node CREATED="1385553963308" ID="ID_454085934" MODIFIED="1385553966355" TEXT="automatic?"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 <node CREATED="1385553972519" ID="ID_1468748078" MODIFIED="1385553979196" TEXT="unspeficed example"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 <node CREATED="1385553312419" ID="ID_570137281" MODIFIED="1385553316034" TEXT="record">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 <node CREATED="1385553316404" ID="ID_1584846061" MODIFIED="1385553329979" TEXT="descipbing mathematical construct"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
71 <node CREATED="1385554082422" ID="ID_1122297353" MODIFIED="1385554088641" TEXT="sntandard procedure">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 <node CREATED="1385554130413" ID="ID_170791825" MODIFIED="1385554140797" TEXT="to show the existence of the record"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 <node CREATED="1385554092447" ID="ID_1172230634" MODIFIED="1385554100198" TEXT="define record"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74 <node CREATED="1385554100656" ID="ID_1463057859" MODIFIED="1385554109327" TEXT="describe field"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75 <node CREATED="1385554109800" ID="ID_1363129826" MODIFIED="1385554115073" TEXT="proof filed"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 <node CREATED="1385552973397" ID="ID_975113480" MODIFIED="1385554244732" TEXT="where to put variables?">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 <node CREATED="1385552981158" ID="ID_271531253" MODIFIED="1385552985460" TEXT="equalizer"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
79 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
81 <node CREATED="1385553337511" ID="ID_375830623" MODIFIED="1385553340044" TEXT="lemma">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
82 <node CREATED="1385553340598" ID="ID_1472759359" MODIFIED="1385553342884" TEXT="theorem"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
83 <node CREATED="1385553343847" ID="ID_1243315508" MODIFIED="1385553350226" TEXT="input"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
84 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 <node CREATED="1385552588272" ID="ID_102481863" MODIFIED="1385552600054" TEXT="unproofbable theorem">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 <node CREATED="1385552600714" ID="ID_310970637" MODIFIED="1385552682204" TEXT="functional extensionarity "/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
87 <node CREATED="1385552710574" ID="ID_1830254576" MODIFIED="1385552716716" TEXT="congulurence"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 <node CREATED="1385552778933" ID="ID_111669053" MODIFIED="1385552786125" TEXT="type inconsistency">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 <node CREATED="1385552786679" ID="ID_463662714" MODIFIED="1385552788556" TEXT="red"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
91 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
92 <node CREATED="1385552790550" ID="ID_1875122156" MODIFIED="1385552814210" TEXT="insufficent instanciation">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
93 <node CREATED="1385552814757" ID="ID_1350447565" MODIFIED="1385552817194" TEXT="yellow"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
94 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
95 <node CREATED="1385553372431" ID="ID_922931873" MODIFIED="1385553392411" TEXT="make implict variable explicit">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96 <node CREATED="1385553402940" ID="ID_1458630954" MODIFIED="1385553409689" TEXT="in lambda parameter"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 <node CREATED="1385553033119" ID="ID_848845946" MODIFIED="1385553036165" TEXT="module">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 <node CREATED="1385553037809" ID="ID_1708974052" MODIFIED="1385553041116" TEXT="module parameter"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
100 <node CREATED="1385553043977" ID="ID_106475876" MODIFIED="1385553054929" TEXT="mono-morphism">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
101 <node CREATED="1385553057444" ID="ID_548012657" MODIFIED="1385553064202" TEXT="strange symbols"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
102 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
103 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
104 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
105 <node CREATED="1384158677282" ID="ID_174231957" MODIFIED="1385552419537" POSITION="left" TEXT="mathematical thinking">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 <node CREATED="1384158684403" ID="ID_1399570192" MODIFIED="1384158689741" TEXT="understanding"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
107 <node CREATED="1385552451013" ID="ID_831968301" MODIFIED="1385552457147" TEXT="pattern matching"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
108 <node CREATED="1385552461182" ID="ID_220420516" MODIFIED="1385552466866" TEXT="problem solving">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 <node CREATED="1385552466866" ID="ID_781175552" MODIFIED="1385552473172" TEXT="proof finding"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
110 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
111 <node CREATED="1385552477803" ID="ID_1460716599" MODIFIED="1385552482511" TEXT="problem finding"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
113 <node CREATED="1385552909317" ID="ID_1707994061" MODIFIED="1385552914641" POSITION="left" TEXT="usefulness of Agda">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
114 <node CREATED="1385552915662" ID="ID_643691875" MODIFIED="1385552927413" TEXT="to complete understandings"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 <node CREATED="1385552934325" ID="ID_133712397" MODIFIED="1385552943388" TEXT="see the proof symmetrry"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
116 <node CREATED="1385552951917" ID="ID_1111590064" MODIFIED="1385552962300" TEXT="find proof"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
117 <node CREATED="1385553232568" ID="ID_468716239" MODIFIED="1385553237087" TEXT="all manual">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
118 <node CREATED="1385553237769" ID="ID_1111001659" MODIFIED="1385553241551" TEXT="no tactics"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 <node CREATED="1385553247808" ID="ID_1663360868" MODIFIED="1385553251590" TEXT="visible proof"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121 <node CREATED="1385553266033" ID="ID_1734836012" MODIFIED="1385553271207" TEXT="proof is very personal">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 <node CREATED="1385553272594" ID="ID_1133435953" MODIFIED="1385553275976" TEXT="special symbols"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123 <node CREATED="1385553278491" ID="ID_1356974254" MODIFIED="1385553295237" TEXT="customaization of equations and transformation"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
124 <node CREATED="1385553706422" ID="ID_364674985" MODIFIED="1385553716075" TEXT="module parameter selection"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
125 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
126 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
127 <node CREATED="1385553189860" ID="ID_867277383" MODIFIED="1385553192010" POSITION="left" TEXT="How to use">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
128 <node CREATED="1385553195958" ID="ID_286425960" MODIFIED="1385553205471" TEXT="to understand Cateogory theory">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
129 <node CREATED="1385553734186" ID="ID_1768850276" MODIFIED="1385553736159" TEXT="Monad"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
130 <node CREATED="1385553737601" ID="ID_1237992091" MODIFIED="1385553742471" TEXT="Kan extension"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
131 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 <node CREATED="1385553208022" ID="ID_1238219050" MODIFIED="1385553225357" TEXT="Hoare logic like proof of practical programming"/>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
133 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
134 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 </map>