-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Deploying to gh-pages from @ 7d0226d 🚀
- Loading branch information
Showing
6 changed files
with
66 additions
and
68 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,47 +1,45 @@ | ||
| <!DOCTYPE HTML> | ||
| <html><head><meta charset="utf-8"><title>Tactic.Assumption</title><link rel='stylesheet' href='https://cdnjs.cloudflare.com/ajax/libs/github-fork-ribbon-css/0.2.3/gh-fork-ribbon.min.css'/><style>.github-fork-ribbon:before { background-color: #333; }</style><link rel="stylesheet" href="css/Agda.css"></head><body><a class='github-fork-ribbon'href='https://github.com/agda/agda-stdlib-meta/tree/fix-deriving-type-generation///Tactic/Assumption.agda'data-ribbon='Source code on Github' title='Source code on Github'>Source code on Github</a><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--safe</a> <a id="20" class="Pragma">--without-K</a> <a id="32" class="Symbol">#-}</a> | ||
|
|
||
| <a id="37" class="Symbol">{-#</a> <a id="41" class="Keyword">OPTIONS</a> <a id="49" class="Pragma">-v</a> <a id="52" class="Pragma">allTactics:100</a> <a id="67" class="Symbol">#-}</a> | ||
| <a id="71" class="Comment">--------------------------------------------------------------------------------</a> | ||
| <a id="152" class="Comment">-- assumption: try to solve the goal with one of the available assumptions</a> | ||
| <a id="227" class="Comment">--------------------------------------------------------------------------------</a> | ||
|
|
||
| <a id="309" class="Keyword">module</a> <a id="316" href="Tactic.Assumption.html" class="Module">Tactic.Assumption</a> <a id="334" class="Keyword">where</a> | ||
|
|
||
| <a id="341" class="Keyword">open</a> <a id="346" class="Keyword">import</a> <a id="353" href="Meta.Prelude.html" class="Module">Meta.Prelude</a> | ||
| <a id="366" class="Keyword">open</a> <a id="371" class="Keyword">import</a> <a id="378" href="Meta.Init.html" class="Module">Meta.Init</a> | ||
|
|
||
| <a id="389" class="Keyword">open</a> <a id="394" class="Keyword">import</a> <a id="401" href="Class.Functor.html" class="Module">Class.Functor</a> | ||
| <a id="415" class="Keyword">open</a> <a id="420" class="Keyword">import</a> <a id="427" href="Class.Monad.html" class="Module">Class.Monad</a> | ||
| <a id="439" class="Keyword">open</a> <a id="444" class="Keyword">import</a> <a id="451" href="Class.MonadError.Instances.html" class="Module">Class.MonadError.Instances</a> | ||
| <a id="478" class="Keyword">open</a> <a id="483" class="Keyword">import</a> <a id="490" href="Class.MonadReader.Instances.html" class="Module">Class.MonadReader.Instances</a> | ||
| <a id="518" class="Keyword">open</a> <a id="523" class="Keyword">import</a> <a id="530" href="Class.MonadTC.Instances.html" class="Module">Class.MonadTC.Instances</a> | ||
|
|
||
| <a id="555" class="Keyword">open</a> <a id="560" class="Keyword">import</a> <a id="567" href="Reflection.Tactic.html" class="Module">Reflection.Tactic</a> | ||
| <a id="585" class="Keyword">open</a> <a id="590" class="Keyword">import</a> <a id="597" href="Reflection.Utils.html" class="Module">Reflection.Utils</a> | ||
| <a id="614" class="Keyword">open</a> <a id="619" class="Keyword">import</a> <a id="626" href="Reflection.Utils.TCI.html" class="Module">Reflection.Utils.TCI</a> | ||
|
|
||
| <a id="648" class="Keyword">instance</a> | ||
| <a id="659" href="Tactic.Assumption.html#659" class="Function">_</a> <a id="661" class="Symbol">=</a> <a id="663" href="Class.Monad.Core.html#610" class="Function">Functor-M</a> | ||
|
|
||
| <a id="assumption'"></a><a id="674" href="Tactic.Assumption.html#674" class="Function">assumption'</a> <a id="686" class="Symbol">:</a> <a id="688" href="Reflection.Tactic.html#540" class="Function">ITactic</a> | ||
| <a id="696" href="Tactic.Assumption.html#674" class="Function">assumption'</a> <a id="708" class="Symbol">=</a> <a id="710" href="Reflection.Utils.TCI.html#5951" class="Function">inDebugPath</a> <a id="722" class="String">"assumption"</a> <a id="735" class="Keyword">do</a> | ||
| <a id="740" href="Tactic.Assumption.html#740" class="Bound">c</a> <a id="742" href="Class.Monad.Core.html#290" class="Field Operator">←</a> <a id="744" href="Class.MonadTC.html#10565" class="Function">getContext</a> | ||
| <a id="757" href="Data.List.Base.html#4249" class="Function">foldl</a> <a id="763" class="Symbol">(λ</a> <a id="766" href="Tactic.Assumption.html#766" class="Bound">x</a> <a id="768" href="Tactic.Assumption.html#768" class="Bound">k</a> <a id="770" class="Symbol">→</a> <a id="772" class="Keyword">do</a> | ||
| <a id="779" href="Class.MonadError.html#364" class="Field">catch</a> <a id="785" class="Symbol">(</a><a id="786" href="Class.MonadTC.html#13009" class="Function">unifyWithGoal</a> <a id="800" class="Symbol">(</a><a id="801" href="Reflection.Syntax.html#1453" class="InductiveConstructor">♯</a> <a id="803" href="Tactic.Assumption.html#768" class="Bound">k</a><a id="804" class="Symbol">)</a> <a id="806" href="Class.Monad.Core.html#324" class="Function Operator">>></a> <a id="809" href="Class.MonadTC.html#8261" class="Function">debugLog</a> <a id="818" class="Symbol">(</a><a id="819" class="String">"Success with: "</a> <a id="836" href="Reflection.Debug.html#1115" class="Function Operator">∷ᵈ</a> <a id="839" href="Reflection.Syntax.html#1453" class="InductiveConstructor">♯</a> <a id="841" href="Tactic.Assumption.html#768" class="Bound">k</a> <a id="843" href="Reflection.Debug.html#1115" class="Function Operator">∷ᵈ</a> <a id="846" href="Agda.Builtin.List.html#184" class="InductiveConstructor">[]</a><a id="848" class="Symbol">))</a> <a id="851" class="Symbol">(λ</a> <a id="854" href="Tactic.Assumption.html#854" class="Bound">_</a> <a id="856" class="Symbol">→</a> <a id="858" href="Tactic.Assumption.html#766" class="Bound">x</a><a id="859" class="Symbol">))</a> | ||
| <a id="866" class="Symbol">(</a><a id="867" href="Class.MonadTC.html#11406" class="Function">logAndError1</a> <a id="880" class="String">"No valid assumption!"</a><a id="902" class="Symbol">)</a> <a id="904" class="Symbol">(</a><a id="905" href="Data.List.Base.html#6728" class="Function">downFrom</a> <a id="914" href="Function.Base.html#1974" class="Function Operator">$</a> <a id="916" href="Data.List.Base.html#5044" class="Function">length</a> <a id="923" href="Tactic.Assumption.html#740" class="Bound">c</a><a id="924" class="Symbol">)</a> | ||
|
|
||
| <a id="927" class="Keyword">module</a> <a id="934" href="Tactic.Assumption.html#934" class="Module">_</a> <a id="936" class="Symbol">⦃</a> <a id="938" href="Tactic.Assumption.html#938" class="Bound">_</a> <a id="940" class="Symbol">:</a> <a id="942" href="Class.MonadTC.html#666" class="Record">TCOptions</a> <a id="952" class="Symbol">⦄</a> <a id="954" class="Keyword">where</a> | ||
| <a id="962" class="Keyword">macro</a> | ||
| <a id="972" href="Tactic.Assumption.html#972" class="Function">assumption</a> <a id="983" class="Symbol">=</a> <a id="985" href="Reflection.Tactic.html#843" class="Function">initTac</a> <a id="993" href="Tactic.Assumption.html#674" class="Function">assumption'</a> | ||
| <a id="1009" href="Tactic.Assumption.html#1009" class="Function">assumptionOpts</a> <a id="1024" class="Symbol">=</a> <a id="1026" href="Reflection.Tactic.html#682" class="Function">initTacOpts</a> <a id="1038" href="Tactic.Assumption.html#674" class="Function">assumption'</a> | ||
|
|
||
| <a id="1051" class="Keyword">private</a> | ||
| <a id="1061" class="Keyword">open</a> <a id="1066" class="Keyword">import</a> <a id="1073" href="Tactic.Defaults.html" class="Module">Tactic.Defaults</a> | ||
| <a id="1091" class="Keyword">module</a> <a id="Test"></a><a id="1098" href="Tactic.Assumption.html#1098" class="Module">Test</a> <a id="1103" class="Keyword">where</a> | ||
| <a id="Test.test₁"></a><a id="1113" href="Tactic.Assumption.html#1113" class="Function">test₁</a> <a id="1119" class="Symbol">:</a> <a id="1121" class="Symbol">{</a><a id="1122" href="Tactic.Assumption.html#1122" class="Bound">A</a> <a id="1124" href="Tactic.Assumption.html#1124" class="Bound">B</a> <a id="1126" class="Symbol">:</a> <a id="1128" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="1131" class="Symbol">}</a> <a id="1133" class="Symbol">→</a> <a id="1135" href="Tactic.Assumption.html#1122" class="Bound">A</a> <a id="1137" class="Symbol">→</a> <a id="1139" href="Tactic.Assumption.html#1124" class="Bound">B</a> <a id="1141" class="Symbol">→</a> <a id="1143" href="Tactic.Assumption.html#1122" class="Bound">A</a> | ||
| <a id="1149" href="Tactic.Assumption.html#1113" class="Function">test₁</a> <a id="1155" href="Tactic.Assumption.html#1155" class="Bound">a</a> <a id="1157" href="Tactic.Assumption.html#1157" class="Bound">b</a> <a id="1159" class="Symbol">=</a> <a id="1161" href="Tactic.Assumption.html#972" class="Macro">assumption</a> | ||
|
|
||
| <a id="Test.test₂"></a><a id="1177" href="Tactic.Assumption.html#1177" class="Function">test₂</a> <a id="1183" class="Symbol">:</a> <a id="1185" class="Symbol">{</a><a id="1186" href="Tactic.Assumption.html#1186" class="Bound">A</a> <a id="1188" href="Tactic.Assumption.html#1188" class="Bound">B</a> <a id="1190" class="Symbol">:</a> <a id="1192" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="1195" class="Symbol">}</a> <a id="1197" class="Symbol">→</a> <a id="1199" href="Tactic.Assumption.html#1186" class="Bound">A</a> <a id="1201" class="Symbol">→</a> <a id="1203" href="Tactic.Assumption.html#1188" class="Bound">B</a> <a id="1205" class="Symbol">→</a> <a id="1207" href="Tactic.Assumption.html#1188" class="Bound">B</a> | ||
| <a id="1213" href="Tactic.Assumption.html#1177" class="Function">test₂</a> <a id="1219" href="Tactic.Assumption.html#1219" class="Bound">a</a> <a id="1221" href="Tactic.Assumption.html#1221" class="Bound">b</a> <a id="1223" class="Symbol">=</a> <a id="1225" href="Tactic.Assumption.html#972" class="Macro">assumption</a> | ||
| <a id="36" class="Comment">--------------------------------------------------------------------------------</a> | ||
| <a id="117" class="Comment">-- assumption: try to solve the goal with one of the available assumptions</a> | ||
| <a id="192" class="Comment">--------------------------------------------------------------------------------</a> | ||
|
|
||
| <a id="274" class="Keyword">module</a> <a id="281" href="Tactic.Assumption.html" class="Module">Tactic.Assumption</a> <a id="299" class="Keyword">where</a> | ||
|
|
||
| <a id="306" class="Keyword">open</a> <a id="311" class="Keyword">import</a> <a id="318" href="Meta.Prelude.html" class="Module">Meta.Prelude</a> | ||
| <a id="331" class="Keyword">open</a> <a id="336" class="Keyword">import</a> <a id="343" href="Meta.Init.html" class="Module">Meta.Init</a> | ||
|
|
||
| <a id="354" class="Keyword">open</a> <a id="359" class="Keyword">import</a> <a id="366" href="Class.Functor.html" class="Module">Class.Functor</a> | ||
| <a id="380" class="Keyword">open</a> <a id="385" class="Keyword">import</a> <a id="392" href="Class.Monad.html" class="Module">Class.Monad</a> | ||
| <a id="404" class="Keyword">open</a> <a id="409" class="Keyword">import</a> <a id="416" href="Class.MonadError.Instances.html" class="Module">Class.MonadError.Instances</a> | ||
| <a id="443" class="Keyword">open</a> <a id="448" class="Keyword">import</a> <a id="455" href="Class.MonadReader.Instances.html" class="Module">Class.MonadReader.Instances</a> | ||
| <a id="483" class="Keyword">open</a> <a id="488" class="Keyword">import</a> <a id="495" href="Class.MonadTC.Instances.html" class="Module">Class.MonadTC.Instances</a> | ||
|
|
||
| <a id="520" class="Keyword">open</a> <a id="525" class="Keyword">import</a> <a id="532" href="Reflection.Tactic.html" class="Module">Reflection.Tactic</a> | ||
| <a id="550" class="Keyword">open</a> <a id="555" class="Keyword">import</a> <a id="562" href="Reflection.Utils.html" class="Module">Reflection.Utils</a> | ||
| <a id="579" class="Keyword">open</a> <a id="584" class="Keyword">import</a> <a id="591" href="Reflection.Utils.TCI.html" class="Module">Reflection.Utils.TCI</a> | ||
|
|
||
| <a id="613" class="Keyword">instance</a> | ||
| <a id="624" href="Tactic.Assumption.html#624" class="Function">_</a> <a id="626" class="Symbol">=</a> <a id="628" href="Class.Monad.Core.html#610" class="Function">Functor-M</a> | ||
|
|
||
| <a id="assumption'"></a><a id="639" href="Tactic.Assumption.html#639" class="Function">assumption'</a> <a id="651" class="Symbol">:</a> <a id="653" href="Reflection.Tactic.html#540" class="Function">ITactic</a> | ||
| <a id="661" href="Tactic.Assumption.html#639" class="Function">assumption'</a> <a id="673" class="Symbol">=</a> <a id="675" href="Reflection.Utils.TCI.html#5951" class="Function">inDebugPath</a> <a id="687" class="String">"assumption"</a> <a id="700" class="Keyword">do</a> | ||
| <a id="705" href="Tactic.Assumption.html#705" class="Bound">c</a> <a id="707" href="Class.Monad.Core.html#290" class="Field Operator">←</a> <a id="709" href="Class.MonadTC.html#10565" class="Function">getContext</a> | ||
| <a id="722" href="Data.List.Base.html#4249" class="Function">foldl</a> <a id="728" class="Symbol">(λ</a> <a id="731" href="Tactic.Assumption.html#731" class="Bound">x</a> <a id="733" href="Tactic.Assumption.html#733" class="Bound">k</a> <a id="735" class="Symbol">→</a> <a id="737" class="Keyword">do</a> | ||
| <a id="744" href="Class.MonadError.html#364" class="Field">catch</a> <a id="750" class="Symbol">(</a><a id="751" href="Class.MonadTC.html#13009" class="Function">unifyWithGoal</a> <a id="765" class="Symbol">(</a><a id="766" href="Reflection.Syntax.html#1453" class="InductiveConstructor">♯</a> <a id="768" href="Tactic.Assumption.html#733" class="Bound">k</a><a id="769" class="Symbol">)</a> <a id="771" href="Class.Monad.Core.html#324" class="Function Operator">>></a> <a id="774" href="Class.MonadTC.html#8261" class="Function">debugLog</a> <a id="783" class="Symbol">(</a><a id="784" class="String">"Success with: "</a> <a id="801" href="Reflection.Debug.html#1115" class="Function Operator">∷ᵈ</a> <a id="804" href="Reflection.Syntax.html#1453" class="InductiveConstructor">♯</a> <a id="806" href="Tactic.Assumption.html#733" class="Bound">k</a> <a id="808" href="Reflection.Debug.html#1115" class="Function Operator">∷ᵈ</a> <a id="811" href="Agda.Builtin.List.html#184" class="InductiveConstructor">[]</a><a id="813" class="Symbol">))</a> <a id="816" class="Symbol">(λ</a> <a id="819" href="Tactic.Assumption.html#819" class="Bound">_</a> <a id="821" class="Symbol">→</a> <a id="823" href="Tactic.Assumption.html#731" class="Bound">x</a><a id="824" class="Symbol">))</a> | ||
| <a id="831" class="Symbol">(</a><a id="832" href="Class.MonadTC.html#11406" class="Function">logAndError1</a> <a id="845" class="String">"No valid assumption!"</a><a id="867" class="Symbol">)</a> <a id="869" class="Symbol">(</a><a id="870" href="Data.List.Base.html#6728" class="Function">downFrom</a> <a id="879" href="Function.Base.html#1974" class="Function Operator">$</a> <a id="881" href="Data.List.Base.html#5044" class="Function">length</a> <a id="888" href="Tactic.Assumption.html#705" class="Bound">c</a><a id="889" class="Symbol">)</a> | ||
|
|
||
| <a id="892" class="Keyword">module</a> <a id="899" href="Tactic.Assumption.html#899" class="Module">_</a> <a id="901" class="Symbol">⦃</a> <a id="903" href="Tactic.Assumption.html#903" class="Bound">_</a> <a id="905" class="Symbol">:</a> <a id="907" href="Class.MonadTC.html#666" class="Record">TCOptions</a> <a id="917" class="Symbol">⦄</a> <a id="919" class="Keyword">where</a> | ||
| <a id="927" class="Keyword">macro</a> | ||
| <a id="937" href="Tactic.Assumption.html#937" class="Function">assumption</a> <a id="948" class="Symbol">=</a> <a id="950" href="Reflection.Tactic.html#843" class="Function">initTac</a> <a id="958" href="Tactic.Assumption.html#639" class="Function">assumption'</a> | ||
| <a id="974" href="Tactic.Assumption.html#974" class="Function">assumptionOpts</a> <a id="989" class="Symbol">=</a> <a id="991" href="Reflection.Tactic.html#682" class="Function">initTacOpts</a> <a id="1003" href="Tactic.Assumption.html#639" class="Function">assumption'</a> | ||
|
|
||
| <a id="1016" class="Keyword">private</a> | ||
| <a id="1026" class="Keyword">open</a> <a id="1031" class="Keyword">import</a> <a id="1038" href="Tactic.Defaults.html" class="Module">Tactic.Defaults</a> | ||
| <a id="1056" class="Keyword">module</a> <a id="Test"></a><a id="1063" href="Tactic.Assumption.html#1063" class="Module">Test</a> <a id="1068" class="Keyword">where</a> | ||
| <a id="Test.test₁"></a><a id="1078" href="Tactic.Assumption.html#1078" class="Function">test₁</a> <a id="1084" class="Symbol">:</a> <a id="1086" class="Symbol">{</a><a id="1087" href="Tactic.Assumption.html#1087" class="Bound">A</a> <a id="1089" href="Tactic.Assumption.html#1089" class="Bound">B</a> <a id="1091" class="Symbol">:</a> <a id="1093" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="1096" class="Symbol">}</a> <a id="1098" class="Symbol">→</a> <a id="1100" href="Tactic.Assumption.html#1087" class="Bound">A</a> <a id="1102" class="Symbol">→</a> <a id="1104" href="Tactic.Assumption.html#1089" class="Bound">B</a> <a id="1106" class="Symbol">→</a> <a id="1108" href="Tactic.Assumption.html#1087" class="Bound">A</a> | ||
| <a id="1114" href="Tactic.Assumption.html#1078" class="Function">test₁</a> <a id="1120" href="Tactic.Assumption.html#1120" class="Bound">a</a> <a id="1122" href="Tactic.Assumption.html#1122" class="Bound">b</a> <a id="1124" class="Symbol">=</a> <a id="1126" href="Tactic.Assumption.html#937" class="Macro">assumption</a> | ||
|
|
||
| <a id="Test.test₂"></a><a id="1142" href="Tactic.Assumption.html#1142" class="Function">test₂</a> <a id="1148" class="Symbol">:</a> <a id="1150" class="Symbol">{</a><a id="1151" href="Tactic.Assumption.html#1151" class="Bound">A</a> <a id="1153" href="Tactic.Assumption.html#1153" class="Bound">B</a> <a id="1155" class="Symbol">:</a> <a id="1157" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="1160" class="Symbol">}</a> <a id="1162" class="Symbol">→</a> <a id="1164" href="Tactic.Assumption.html#1151" class="Bound">A</a> <a id="1166" class="Symbol">→</a> <a id="1168" href="Tactic.Assumption.html#1153" class="Bound">B</a> <a id="1170" class="Symbol">→</a> <a id="1172" href="Tactic.Assumption.html#1153" class="Bound">B</a> | ||
| <a id="1178" href="Tactic.Assumption.html#1142" class="Function">test₂</a> <a id="1184" href="Tactic.Assumption.html#1184" class="Bound">a</a> <a id="1186" href="Tactic.Assumption.html#1186" class="Bound">b</a> <a id="1188" class="Symbol">=</a> <a id="1190" href="Tactic.Assumption.html#937" class="Macro">assumption</a> | ||
| </pre></body></html> |
Oops, something went wrong.