Commit 75250380 authored by André Pacak's avatar André Pacak

do not use match_Fun judgment anymore

parent 99e59e7b
......@@ -60,6 +60,10 @@
<child id="2973820376015605589" name="conclusion" index="1FvUUP" />
<child id="2973820376015605556" name="premises" index="1FvUVk" />
</concept>
<concept id="3351376301269548860" name="TypeLang.structure.JudgmentInstanceMatch" flags="ng" index="1RlKn1">
<child id="3351376301269548861" name="term" index="1RlKn0" />
<child id="3351376301269548862" name="pat" index="1RlKn3" />
</concept>
<concept id="3351376301258987589" name="TypeLang.structure.Sort" flags="ng" index="1RHyaS">
<child id="2973820376015170130" name="mode" index="1FtGIM" />
</concept>
......@@ -149,30 +153,6 @@
<node concept="1FtGIT" id="2U2uJPpfXBf" role="1FtGIM" />
</node>
</node>
<node concept="1F53FG" id="7TgNhRbtzUB" role="1FufQt" />
<node concept="1FvzHF" id="6G$bWLkr_bK" role="1FufQt">
<property role="TrG5h" value="match_Fun" />
<node concept="1FtGIX" id="6G$bWLkr_bL" role="1FvzHG" />
<node concept="1FtGBS" id="6G$bWLkr_bM" role="1FvzHH">
<ref role="1FtGBW" to="5va7:1Da9ityUTef" resolve="Type" />
<node concept="1FtGIS" id="2U2uJPpfXBi" role="1FtGIM" />
</node>
<node concept="1FtGIX" id="6G$bWLkr_bO" role="1FvzTf">
<property role="1FtGIY" value="match_Fun" />
</node>
<node concept="1FtGBS" id="6G$bWLkr_bP" role="1FvzHI">
<ref role="1FtGBW" to="5va7:1Da9ityUTef" resolve="Type" />
<node concept="1FtGIT" id="2U2uJPpfXBl" role="1FtGIM" />
</node>
<node concept="1FtGIX" id="6G$bWLkr_bR" role="1FsQh1">
<property role="1FtGIY" value="-&gt;" />
</node>
<node concept="1FtGBS" id="6G$bWLkr_bS" role="1FvzHK">
<ref role="1FtGBW" to="5va7:1Da9ityUTef" resolve="Type" />
<node concept="1FtGIT" id="2U2uJPpfXBo" role="1FtGIM" />
</node>
<node concept="1FtGIX" id="6G$bWLkr_bU" role="1FvzSA" />
</node>
<node concept="1F53FG" id="6G$bWLkr_bW" role="1FufQt" />
<node concept="1FvUVj" id="6G$bWLkr_bX" role="1FufQt">
<property role="TrG5h" value="infer Zero" />
......@@ -331,20 +311,20 @@
<node concept="1FvUUU" id="6G$bWLkr_cO" role="1FvB8I">
<property role="TrG5h" value="t1" />
</node>
<node concept="1FvUUU" id="6G$bWLkr_cP" role="1FvB8J">
<property role="TrG5h" value="ty" />
</node>
</node>
<node concept="1FvB8F" id="6G$bWLkr_cQ" role="1FvUVk">
<ref role="1FvB8G" node="6G$bWLkr_bK" resolve="match_Fun" />
<node concept="1FvUUU" id="6G$bWLkr_cR" role="1FvB8H">
<property role="TrG5h" value="ty" />
</node>
<node concept="1FvUUU" id="6G$bWLkr_cS" role="1FvB8I">
<property role="TrG5h" value="ty1" />
</node>
<node concept="1FvUUU" id="6G$bWLkr_cT" role="1FvB8J">
<property role="TrG5h" value="ty2" />
<node concept="27Pwox" id="6OMXo1Tn0f4" role="1FvB8J">
<ref role="1F1YRu" to="5va7:1Da9ityUTeg" resolve="Fun" />
<node concept="bFJCQ" id="6OMXo1Tn0f5" role="27Pwov">
<ref role="3zVwH8" to="5va7:1Da9ityUTel" resolve="ty1" />
<node concept="1FvUUU" id="6OMXo1Tn0f6" role="bFJCb">
<property role="TrG5h" value="ty1" />
</node>
</node>
<node concept="bFJCQ" id="6OMXo1Tn0f7" role="27Pwov">
<ref role="3zVwH8" to="5va7:1Da9ityUTep" resolve="ty2" />
<node concept="1FvUUU" id="6OMXo1Tn0f8" role="bFJCb">
<property role="TrG5h" value="ty2" />
</node>
</node>
</node>
</node>
<node concept="1FvB8F" id="6G$bWLkr_cU" role="1FvUVk">
......@@ -399,6 +379,26 @@
<node concept="1F53FG" id="6G$bWLkr_dc" role="1FufQt" />
<node concept="1FvUVj" id="6G$bWLkr_dd" role="1FufQt">
<property role="TrG5h" value="check Lam" />
<node concept="1RlKn1" id="mSp$0_t5HY" role="1FvUVk">
<node concept="1FvUUU" id="mSp$0_t5IG" role="1RlKn0">
<property role="TrG5h" value="ty" />
</node>
<node concept="27Pwox" id="mSp$0_t5IJ" role="1RlKn3">
<ref role="1F1YRu" to="5va7:1Da9ityUTeg" resolve="Fun" />
<node concept="bFJCQ" id="mSp$0_t5IK" role="27Pwov">
<ref role="3zVwH8" to="5va7:1Da9ityUTel" resolve="ty1" />
<node concept="1FvUUU" id="mSp$0_t5IL" role="bFJCb">
<property role="TrG5h" value="ty1" />
</node>
</node>
<node concept="bFJCQ" id="mSp$0_t5IM" role="27Pwov">
<ref role="3zVwH8" to="5va7:1Da9ityUTep" resolve="ty2" />
<node concept="1FvUUU" id="mSp$0_t5IN" role="bFJCb">
<property role="TrG5h" value="ty2" />
</node>
</node>
</node>
</node>
<node concept="1FvB8F" id="6G$bWLkr_de" role="1FvUUP">
<ref role="1FvB8G" node="6G$bWLkr_bq" resolve="check" />
<node concept="1FvUUU" id="6G$bWLkr_df" role="1FvB8H">
......@@ -423,18 +423,6 @@
<property role="TrG5h" value="ty" />
</node>
</node>
<node concept="1FvB8F" id="6G$bWLkspyV" role="1FvUVk">
<ref role="1FvB8G" node="6G$bWLkr_bK" resolve="match_Fun" />
<node concept="1FvUUU" id="6G$bWLksp$4" role="1FvB8H">
<property role="TrG5h" value="ty" />
</node>
<node concept="1FvUUU" id="6G$bWLksp$g" role="1FvB8I">
<property role="TrG5h" value="ty1" />
</node>
<node concept="1FvUUU" id="6G$bWLksp$s" role="1FvB8J">
<property role="TrG5h" value="ty2" />
</node>
</node>
<node concept="1FvB8F" id="6G$bWLkr_dq" role="1FvUVk">
<ref role="1FvB8G" node="6G$bWLkr_bq" resolve="check" />
<node concept="27Pwox" id="6G$bWLkr_dr" role="1FvB8H">
......@@ -504,35 +492,6 @@
</node>
<node concept="1F53FG" id="6G$bWLkr_dI" role="1FufQt" />
<node concept="1F53FG" id="6G$bWLkr_dJ" role="1FufQt" />
<node concept="1F53FG" id="6G$bWLkr_dK" role="1FufQt" />
<node concept="1FvUVj" id="6G$bWLkr_dL" role="1FufQt">
<property role="TrG5h" value="match Fun" />
<node concept="1FvB8F" id="6G$bWLkr_dM" role="1FvUUP">
<ref role="1FvB8G" node="6G$bWLkr_bK" resolve="match_Fun" />
<node concept="27Pwox" id="6G$bWLkr_dN" role="1FvB8H">
<ref role="1F1YRu" to="5va7:1Da9ityUTeg" resolve="Fun" />
<node concept="bFJCQ" id="6G$bWLkr_dO" role="27Pwov">
<ref role="3zVwH8" to="5va7:1Da9ityUTel" resolve="ty1" />
<node concept="1FvUUU" id="6G$bWLkr_dP" role="bFJCb">
<property role="TrG5h" value="ty1" />
</node>
</node>
<node concept="bFJCQ" id="6G$bWLkr_dQ" role="27Pwov">
<ref role="3zVwH8" to="5va7:1Da9ityUTep" resolve="ty2" />
<node concept="1FvUUU" id="6G$bWLkr_dR" role="bFJCb">
<property role="TrG5h" value="ty2" />
</node>
</node>
</node>
<node concept="1FvUUU" id="6G$bWLkr_dS" role="1FvB8I">
<property role="TrG5h" value="ty1" />
</node>
<node concept="1FvUUU" id="6G$bWLkr_dT" role="1FvB8J">
<property role="TrG5h" value="ty2" />
</node>
</node>
</node>
<node concept="1F53FG" id="6G$bWLkr_dV" role="1FufQt" />
<node concept="1F53FG" id="7TgNhRbt$1w" role="1FufQt" />
<node concept="1FvUVj" id="2U2uJPq7S1I" role="1FufQt">
<property role="TrG5h" value="lookup found" />
......@@ -614,7 +573,7 @@
<node concept="bFJCQ" id="6OMXo1T_mhh" role="27Pwov">
<ref role="3zVwH8" to="5va7:2_58u12slbe" resolve="type" />
<node concept="1FvUUU" id="6OMXo1T_mhz" role="bFJCb">
<property role="TrG5h" value="ty" />
<property role="TrG5h" value="ty2" />
</node>
</node>
<node concept="bFJCQ" id="6OMXo1T_mhA" role="27Pwov">
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment