Skip to content

Commit

Permalink
Deploying to gh-pages from @ 4125a76 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@WhatisRT
WhatisRT committed Nov 28, 2024
1 parent 1b7eee5 commit 865f27d
Show file tree
Hide file tree
Showing 6 changed files with 344 additions and 355 deletions.
14 changes: 7 additions & 7 deletions Tactic.Case.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,25 +22,25 @@

<a id="552" class="Keyword">instance</a>
<a id="563" href="Tactic.Case.html#563" class="Function">_</a> <a id="565" class="Symbol">=</a> <a id="567" href="Reflection.TCI.html#4289" class="Function">MonadTC-TCI</a>
<a id="581" href="Tactic.Case.html#581" class="Function">_</a> <a id="583" class="Symbol">=</a> <a id="585" href="Tactic.ClauseBuilder.html#11098" class="Function">ContextMonad-MonadTC</a>
<a id="581" href="Tactic.Case.html#581" class="Function">_</a> <a id="583" class="Symbol">=</a> <a id="585" href="Tactic.ClauseBuilder.html#10734" class="Function">ContextMonad-MonadTC</a>
<a id="608" href="Tactic.Case.html#608" class="Function">_</a> <a id="610" class="Symbol">=</a> <a id="612" href="Class.Monad.Core.html#610" class="Function">Functor-M</a>

<a id="623" class="Keyword">open</a> <a id="628" href="Tactic.ClauseBuilder.html#11342" class="Module">ClauseExprM</a>
<a id="623" class="Keyword">open</a> <a id="628" href="Tactic.ClauseBuilder.html#10978" class="Module">ClauseExprM</a>

<a id="matchInductive"></a><a id="641" href="Tactic.Case.html#641" class="Function">matchInductive</a> <a id="656" class="Symbol">:</a> <a id="658" href="Agda.Builtin.Reflection.html#5064" class="Function">Type</a> <a id="663" class="Symbol">→</a> <a id="665" class="Symbol">(</a><a id="666" href="Tactic.ClauseBuilder.html#1679" class="Function">SinglePattern</a> <a id="680" class="Symbol">→</a> <a id="682" href="Reflection.TCI.html#617" class="Function">TC</a> <a id="685" class="Symbol">(</a><a id="686" href="Tactic.ClauseBuilder.html#6171" class="Datatype">ClauseExpr</a> <a id="697" href="Data.Sum.Base.html#625" class="Datatype Operator">⊎</a> <a id="699" href="Agda.Builtin.Maybe.html#135" class="Datatype">Maybe</a> <a id="705" href="Agda.Builtin.Reflection.html#4993" class="Datatype">Term</a><a id="709" class="Symbol">))</a> <a id="712" class="Symbol">→</a> <a id="714" href="Reflection.TCI.html#617" class="Function">TC</a> <a id="717" href="Tactic.ClauseBuilder.html#6171" class="Datatype">ClauseExpr</a>
<a id="matchInductive"></a><a id="641" href="Tactic.Case.html#641" class="Function">matchInductive</a> <a id="656" class="Symbol">:</a> <a id="658" href="Agda.Builtin.Reflection.html#5064" class="Function">Type</a> <a id="663" class="Symbol">→</a> <a id="665" class="Symbol">(</a><a id="666" href="Tactic.ClauseBuilder.html#1351" class="Function">SinglePattern</a> <a id="680" class="Symbol">→</a> <a id="682" href="Reflection.TCI.html#617" class="Function">TC</a> <a id="685" class="Symbol">(</a><a id="686" href="Tactic.ClauseBuilder.html#5843" class="Datatype">ClauseExpr</a> <a id="697" href="Data.Sum.Base.html#625" class="Datatype Operator">⊎</a> <a id="699" href="Agda.Builtin.Maybe.html#135" class="Datatype">Maybe</a> <a id="705" href="Agda.Builtin.Reflection.html#4993" class="Datatype">Term</a><a id="709" class="Symbol">))</a> <a id="712" class="Symbol">→</a> <a id="714" href="Reflection.TCI.html#617" class="Function">TC</a> <a id="717" href="Tactic.ClauseBuilder.html#5843" class="Datatype">ClauseExpr</a>
<a id="728" href="Tactic.Case.html#641" class="Function">matchInductive</a> <a id="743" href="Tactic.Case.html#743" class="Bound">ty</a> <a id="746" href="Tactic.Case.html#746" class="Bound">rhs</a> <a id="750" class="Symbol">=</a> <a id="752" class="Keyword">do</a>
<a id="757" href="Tactic.Case.html#757" class="Bound">ps</a> <a id="760" href="Class.Monad.Core.html#290" class="Field Operator">←</a> <a id="762" href="Tactic.ClauseBuilder.html#5685" class="Function">constructorPatterns&#39;</a> <a id="783" href="Tactic.Case.html#743" class="Bound">ty</a>
<a id="788" href="Tactic.ClauseBuilder.html#11534" class="Function">matchExprM</a> <a id="799" class="Symbol">(</a><a id="800" href="Data.List.Base.html#1634" class="Function">map</a> <a id="804" class="Symbol">(λ</a> <a id="807" href="Tactic.Case.html#807" class="Bound">p</a> <a id="809" class="Symbol">→</a> <a id="811" href="Tactic.Case.html#807" class="Bound">p</a> <a id="813" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="815" href="Tactic.Case.html#746" class="Bound">rhs</a> <a id="819" href="Tactic.Case.html#807" class="Bound">p</a><a id="820" class="Symbol">)</a> <a id="822" href="Tactic.Case.html#757" class="Bound">ps</a><a id="824" class="Symbol">)</a>
<a id="757" href="Tactic.Case.html#757" class="Bound">ps</a> <a id="760" href="Class.Monad.Core.html#290" class="Field Operator">←</a> <a id="762" href="Tactic.ClauseBuilder.html#5357" class="Function">constructorPatterns&#39;</a> <a id="783" href="Tactic.Case.html#743" class="Bound">ty</a>
<a id="788" href="Tactic.ClauseBuilder.html#11170" class="Function">matchExprM</a> <a id="799" class="Symbol">(</a><a id="800" href="Data.List.Base.html#1634" class="Function">map</a> <a id="804" class="Symbol">(λ</a> <a id="807" href="Tactic.Case.html#807" class="Bound">p</a> <a id="809" class="Symbol">→</a> <a id="811" href="Tactic.Case.html#807" class="Bound">p</a> <a id="813" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="815" href="Tactic.Case.html#746" class="Bound">rhs</a> <a id="819" href="Tactic.Case.html#807" class="Bound">p</a><a id="820" class="Symbol">)</a> <a id="822" href="Tactic.Case.html#757" class="Bound">ps</a><a id="824" class="Symbol">)</a>

<a id="genMatchingClauses"></a><a id="827" href="Tactic.Case.html#827" class="Function">genMatchingClauses</a> <a id="846" class="Symbol">:</a> <a id="848" href="Agda.Builtin.Reflection.html#5064" class="Function">Type</a> <a id="853" class="Symbol">→</a> <a id="855" href="Reflection.TCI.html#617" class="Function">TC</a> <a id="858" href="Agda.Builtin.Reflection.html#4993" class="Datatype">Term</a> <a id="863" class="Symbol">→</a> <a id="865" href="Reflection.TCI.html#617" class="Function">TC</a> <a id="868" href="Tactic.ClauseBuilder.html#6171" class="Datatype">ClauseExpr</a>
<a id="genMatchingClauses"></a><a id="827" href="Tactic.Case.html#827" class="Function">genMatchingClauses</a> <a id="846" class="Symbol">:</a> <a id="848" href="Agda.Builtin.Reflection.html#5064" class="Function">Type</a> <a id="853" class="Symbol">→</a> <a id="855" href="Reflection.TCI.html#617" class="Function">TC</a> <a id="858" href="Agda.Builtin.Reflection.html#4993" class="Datatype">Term</a> <a id="863" class="Symbol">→</a> <a id="865" href="Reflection.TCI.html#617" class="Function">TC</a> <a id="868" href="Tactic.ClauseBuilder.html#5843" class="Datatype">ClauseExpr</a>
<a id="879" href="Tactic.Case.html#827" class="Function">genMatchingClauses</a> <a id="898" href="Tactic.Case.html#898" class="Bound">ty</a> <a id="901" href="Tactic.Case.html#901" class="Bound">x</a> <a id="903" class="Symbol">=</a> <a id="905" href="Tactic.Case.html#641" class="Function">matchInductive</a> <a id="920" href="Tactic.Case.html#898" class="Bound">ty</a> <a id="923" class="Symbol">(λ</a> <a id="926" href="Tactic.Case.html#926" class="Bound">_</a> <a id="928" class="Symbol">→</a> <a id="930" class="Symbol">(</a><a id="931" href="Data.Sum.Base.html#700" class="InductiveConstructor">inj₂</a> <a id="936" href="Function.Base.html#1115" class="Function Operator">∘</a> <a id="938" href="Agda.Builtin.Maybe.html#173" class="InductiveConstructor">just</a><a id="942" class="Symbol">)</a> <a id="944" href="Class.Functor.Core.html#233" class="Field Operator">&lt;$&gt;</a> <a id="948" href="Tactic.Case.html#901" class="Bound">x</a><a id="949" class="Symbol">)</a>

<a id="952" class="Comment">-- apply tac to all holes</a>
<a id="case"></a><a id="978" href="Tactic.Case.html#978" class="Function">case</a> <a id="983" class="Symbol">:</a> <a id="985" class="Symbol">∀</a> <a id="987" class="Symbol">{</a><a id="988" href="Tactic.Case.html#988" class="Bound">a</a><a id="989" class="Symbol">}</a> <a id="991" class="Symbol">{</a><a id="992" href="Tactic.Case.html#992" class="Bound">A</a> <a id="994" class="Symbol">:</a> <a id="996" href="Agda.Primitive.html#388" class="Primitive">Set</a> <a id="1000" href="Tactic.Case.html#988" class="Bound">a</a><a id="1001" class="Symbol">}</a> <a id="1003" class="Symbol">→</a> <a id="1005" href="Tactic.Case.html#992" class="Bound">A</a> <a id="1007" class="Symbol">→</a> <a id="1009" href="Reflection.Tactic.html#540" class="Function">ITactic</a> <a id="1017" class="Symbol">→</a> <a id="1019" href="Reflection.Tactic.html#540" class="Function">ITactic</a>
<a id="1027" href="Tactic.Case.html#978" class="Function">case</a> <a id="1032" href="Tactic.Case.html#1032" class="Bound">a</a> <a id="1034" href="Tactic.Case.html#1034" class="Bound">tac</a> <a id="1038" class="Symbol">=</a> <a id="1040" href="Reflection.Utils.TCI.html#5951" class="Function">inDebugPath</a> <a id="1052" class="String">&quot;case&quot;</a> <a id="1059" class="Keyword">do</a>
<a id="1064" href="Tactic.Case.html#1064" class="Bound">t</a> <a id="1066" href="Class.Monad.Core.html#290" class="Field Operator">←</a> <a id="1068" href="Class.MonadTC.html#1953" class="Field">quoteTC</a> <a id="1076" href="Tactic.Case.html#1032" class="Bound">a</a>
<a id="1080" href="Tactic.Case.html#1080" class="Bound">ty</a> <a id="1083" href="Class.Monad.Core.html#290" class="Field Operator">←</a> <a id="1085" href="Class.MonadTC.html#1798" class="Field">inferType</a> <a id="1095" href="Tactic.Case.html#1064" class="Bound">t</a>
<a id="1099" href="Class.MonadTC.html#13009" class="Function">unifyWithGoal</a> <a id="1113" href="Class.Monad.Core.html#379" class="Function Operator">=&lt;&lt;</a> <a id="1117" href="Tactic.ClauseBuilder.html#8947" class="Function">caseMatch</a> <a id="1127" href="Tactic.Case.html#1064" class="Bound">t</a> <a id="1129" class="Symbol">(</a><a id="1130" href="Tactic.Case.html#827" class="Function">genMatchingClauses</a> <a id="1149" href="Tactic.Case.html#1080" class="Bound">ty</a> <a id="1152" class="Symbol">(</a><a id="1153" href="Class.MonadTC.html#13485" class="Function">withGoalHole</a> <a id="1166" href="Tactic.Case.html#1034" class="Bound">tac</a><a id="1169" class="Symbol">))</a>
<a id="1099" href="Class.MonadTC.html#13009" class="Function">unifyWithGoal</a> <a id="1113" href="Class.Monad.Core.html#379" class="Function Operator">=&lt;&lt;</a> <a id="1117" href="Tactic.ClauseBuilder.html#8619" class="Function">caseMatch</a> <a id="1127" href="Tactic.Case.html#1064" class="Bound">t</a> <a id="1129" class="Symbol">(</a><a id="1130" href="Tactic.Case.html#827" class="Function">genMatchingClauses</a> <a id="1149" href="Tactic.Case.html#1080" class="Bound">ty</a> <a id="1152" class="Symbol">(</a><a id="1153" href="Class.MonadTC.html#13485" class="Function">withGoalHole</a> <a id="1166" href="Tactic.Case.html#1034" class="Bound">tac</a><a id="1169" class="Symbol">))</a>

<a id="1173" class="Keyword">private</a>
<a id="1183" class="Keyword">module</a> <a id="Test"></a><a id="1190" href="Tactic.Case.html#1190" class="Module">Test</a> <a id="1195" class="Symbol">(</a><a id="1196" href="Tactic.Case.html#1196" class="Bound">A</a> <a id="1198" href="Tactic.Case.html#1198" class="Bound">B</a> <a id="1200" class="Symbol">:</a> <a id="1202" href="Agda.Primitive.html#388" class="Primitive">Set</a><a id="1205" class="Symbol">)</a> <a id="1207" class="Keyword">where</a>
Expand Down
Loading

0 comments on commit 865f27d

Please sign in to comment.