Mercurial > hg > Papers > 2013 > kono-prosym

annotate Agda.mm @ 2:576a3272522d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
writing...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 01 Dec 2013 17:58:05 +0900
parents 888cc58ced9d
children
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"/>
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
8 <node CREATED="1385597681199" ID="ID_1206471263" MODIFIED="1385597687519" TEXT="executable like Haskell"/>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 <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
11 <node CREATED="1385553144895" ID="ID_5020353" MODIFIED="1385553161258" TEXT="complain nothing is the goal"/>
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
12 <node CREATED="1385597624397" ID="ID_995313728" MODIFIED="1385597661388" TEXT="how fun non executable program?"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
13 </node>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
14 <node CREATED="1385597979683" ID="ID_1830603554" MODIFIED="1385597984087" TEXT="How popular?">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
15 <node CREATED="1385597984088" ID="ID_1047860825" MODIFIED="1385597987107" TEXT="Coq"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
16 <node CREATED="1385597987723" ID="ID_1005518327" MODIFIED="1385598007540" TEXT="Every students use Coq"/>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 </node>
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 CREATED="1384158575905" ID="ID_1857200497" MODIFIED="1384158578202" POSITION="right" TEXT="Proof">
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
20 <node CREATED="1385597911855" ID="ID_226453773" MODIFIED="1385597918132" TEXT="Hayting Algebra"/>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 <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
22 <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
23 <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
24 <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
25 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 <node CREATED="1385552512024" ID="ID_147799666" MODIFIED="1385552516341" POSITION="right" TEXT="Agda Proof System">
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
28 <node CREATED="1385597309971" ID="ID_1759517864" MODIFIED="1385597312786" TEXT="emacs"/>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29 <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
30 <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
31 <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
32 <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
33 <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
34 <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
35 <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
36 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37 <node CREATED="1385552540357" ID="ID_27933366" MODIFIED="1385552542986" TEXT="record"/>
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
38 <node CREATED="1385552532612" ID="ID_40469366" MODIFIED="1385597757862" TEXT="equality">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
39 <node CREATED="1385597173078" ID="ID_503695732" MODIFIED="1385597179382" TEXT="relation"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
40 <node CREATED="1385597180159" ID="ID_366226932" MODIFIED="1385597182662" TEXT="identity"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
41 </node>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 <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
43 <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
44 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
45 <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
46 <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
47 <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
48 </node>
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
49 <node CREATED="1385597581793" ID="ID_560374" MODIFIED="1385597584096" TEXT="all manual">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
50 <node CREATED="1385597584881" ID="ID_1563058814" MODIFIED="1385597593100" TEXT="no haskell support"/>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
51 </node>
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
52 </node>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
53 <node CREATED="1385553423068" ID="ID_1167992721" MODIFIED="1385553433515" POSITION="right" TEXT="Comparing Haskell">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
54 <node CREATED="1385597515449" ID="ID_148577390" MODIFIED="1385597522642" TEXT="strongness of types"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
55 <node CREATED="1385597771461" ID="ID_1284279754" MODIFIED="1385597775740" TEXT="similar syntax"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
56 </node>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
57 <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
58 <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
59 <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
60 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
61 <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
62 <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
63 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 <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
65 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66 <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
67 <node CREATED="1384158660337" ID="ID_1951403393" MODIFIED="1384158666022" TEXT="?">
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 <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
69 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 <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
71 <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
72 <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
73 <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
74 <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
75 <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
76 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 <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
79 <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
80 <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
81 <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
82 <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
83 <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
84 <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
85 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
86 <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
87 <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
88 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 <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
91 <node CREATED="1385553340598" ID="ID_1472759359" MODIFIED="1385553342884" TEXT="theorem"/>
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
92 <node CREATED="1385553343847" ID="ID_1243315508" MODIFIED="1385598120000" TEXT="selecting input arguments"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
93 <node CREATED="1385598122577" ID="ID_1512810213" MODIFIED="1385598134539" TEXT="assumption as input arguments"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
94 </node>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
95 <node CREATED="1385598147877" ID="ID_1767619024" MODIFIED="1385598171099" TEXT="handling not-yet-proved part">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
96 <node CREATED="1385598184783" ID="ID_1082183331" MODIFIED="1385598190881" TEXT="as inpput arguments"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
97 <node CREATED="1385598192184" ID="ID_14552462" MODIFIED="1385598216243" TEXT="postulate"/>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
98 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
99 <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
100 <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
101 <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
102 </node>
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
103 <node CREATED="1385597285233" ID="ID_1903486565" MODIFIED="1385597287428" TEXT="eval">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
104 <node CREATED="1385597287429" ID="ID_1235285760" MODIFIED="1385597292767" TEXT="environment of eval"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
105 </node>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
106 <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
107 <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
108 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
109 <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
110 <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
111 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
112 <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
113 <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
114 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
115 <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
116 <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
117 <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
118 <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
119 </node>
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>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 <node CREATED="1384158677282" ID="ID_174231957" MODIFIED="1385552419537" POSITION="left" TEXT="mathematical thinking">
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
123 <node CREATED="1384158684403" ID="ID_1399570192" MODIFIED="1384158689741" TEXT="understanding">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
124 <node CREATED="1385597890324" ID="ID_1847853272" MODIFIED="1385597941292" TEXT="by types"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
125 <node CREATED="1385597893765" ID="ID_1389031272" MODIFIED="1385597945129" TEXT="by models">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
126 <node CREATED="1385597950001" ID="ID_151641398" MODIFIED="1385597956505" TEXT="not given by Agda"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
127 </node>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
128 </node>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
129 <node CREATED="1385552451013" ID="ID_831968301" MODIFIED="1385552457147" TEXT="pattern matching">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
130 <node CREATED="1385597962784" ID="ID_87138651" MODIFIED="1385597972049" TEXT="is this understandings?"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
131 </node>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
132 <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
133 <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
134 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
135 <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
136 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
137 <node CREATED="1385552909317" ID="ID_1707994061" MODIFIED="1385552914641" POSITION="left" TEXT="usefulness of Agda">
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
138 <node CREATED="1385597697480" ID="ID_895791945" MODIFIED="1385597703669" TEXT="Haskell like syntax">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
139 <node CREATED="1385597717172" ID="ID_1406282220" MODIFIED="1385597721238" TEXT="strange symbols"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
140 <node CREATED="1385597723709" ID="ID_1501399885" MODIFIED="1385597727477" TEXT="emacs support"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
141 </node>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
142 <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
143 <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
144 <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
145 <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
146 <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
147 <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
148 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
149 <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
150 <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
151 <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
152 <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
153 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
154 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
155 <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
156 <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
157 <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
158 <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
159 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
160 <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
161 </node>
1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
162 <node CREATED="1385552342991" ID="ID_1939991054" MODIFIED="1385552354178" POSITION="right" TEXT="Proof by human">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
163 <node CREATED="1385552354669" ID="ID_154501585" MODIFIED="1385552370256" TEXT="wrote at book space">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
164 <node CREATED="1385597411306" ID="ID_41605107" MODIFIED="1385597416033" TEXT="3 lines of proof">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
165 <node CREATED="1385597422045" ID="ID_1465170514" MODIFIED="1385597433982" TEXT="many missing parts"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
166 <node CREATED="1385597436540" ID="ID_1855719075" MODIFIED="1385597452864" TEXT="exercise"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
167 </node>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
168 <node CREATED="1385597804760" ID="ID_552514819" MODIFIED="1385597842300" TEXT="write necessary keywords to recall only"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
169 </node>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
170 <node CREATED="1385552371251" ID="ID_836715929" MODIFIED="1385552382002" TEXT="typed text">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
171 <node CREATED="1385597464732" ID="ID_664600436" MODIFIED="1385597469501" TEXT="missing parts"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
172 <node CREATED="1385597848856" ID="ID_1150238160" MODIFIED="1385597852328" TEXT="formatting problem">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
173 <node CREATED="1385597852600" ID="ID_1735973674" MODIFIED="1385597854304" TEXT="TeX"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
174 <node CREATED="1385597854832" ID="ID_526772293" MODIFIED="1385597862164" TEXT="Commutive diagram"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
175 </node>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
176 </node>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
177 <node CREATED="1385552385336" ID="ID_1562417181" MODIFIED="1385552400070" TEXT="Written in Proof System">
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
178 <node CREATED="1385597474149" ID="ID_1437200348" MODIFIED="1385597476509" TEXT="checked"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
179 <node CREATED="1385597477565" ID="ID_1553409639" MODIFIED="1385597481238" TEXT="have to be complete"/>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
180 </node>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
181 </node>
0
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
182 </node>
aa359e82dab7 Prosym paper 2013
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
183 </map>