diff --git a/Tactic.Assumption.html b/Tactic.Assumption.html index f7dfb0f..9aeb06f 100644 --- a/Tactic.Assumption.html +++ b/Tactic.Assumption.html @@ -1,47 +1,45 @@ Tactic.AssumptionSource code on Github
{-# OPTIONS --safe --without-K #-}
-
-{-# OPTIONS -v allTactics:100 #-}
---------------------------------------------------------------------------------
--- assumption: try to solve the goal with one of the available assumptions
---------------------------------------------------------------------------------
-
-module Tactic.Assumption where
-
-open import Meta.Prelude
-open import Meta.Init
-
-open import Class.Functor
-open import Class.Monad
-open import Class.MonadError.Instances
-open import Class.MonadReader.Instances
-open import Class.MonadTC.Instances
-
-open import Reflection.Tactic
-open import Reflection.Utils
-open import Reflection.Utils.TCI
-
-instance
-  _ = Functor-M
-
-assumption' : ITactic
-assumption' = inDebugPath "assumption" do
-  c ← getContext
-  foldl (λ x k → do
-    catch (unifyWithGoal (♯ k) >> debugLog ("Success with: " ∷ᵈ ♯ k ∷ᵈ [])) (λ _ → x))
-    (logAndError1 "No valid assumption!") (downFrom $ length c)
-
-module _ ⦃ _ : TCOptions ⦄ where
-  macro
-    assumption = initTac assumption'
-    assumptionOpts = initTacOpts assumption'
-
-private
-  open import Tactic.Defaults
-  module Test where
-    test₁ : {A B : Set} → A → B → A
-    test₁ a b = assumption
-
-    test₂ : {A B : Set} → A → B → B
-    test₂ a b = assumption
+--------------------------------------------------------------------------------
+-- assumption: try to solve the goal with one of the available assumptions
+--------------------------------------------------------------------------------
+
+module Tactic.Assumption where
+
+open import Meta.Prelude
+open import Meta.Init
+
+open import Class.Functor
+open import Class.Monad
+open import Class.MonadError.Instances
+open import Class.MonadReader.Instances
+open import Class.MonadTC.Instances
+
+open import Reflection.Tactic
+open import Reflection.Utils
+open import Reflection.Utils.TCI
+
+instance
+  _ = Functor-M
+
+assumption' : ITactic
+assumption' = inDebugPath "assumption" do
+  c ← getContext
+  foldl (λ x k → do
+    catch (unifyWithGoal (♯ k) >> debugLog ("Success with: " ∷ᵈ ♯ k ∷ᵈ [])) (λ _ → x))
+    (logAndError1 "No valid assumption!") (downFrom $ length c)
+
+module _ ⦃ _ : TCOptions ⦄ where
+  macro
+    assumption = initTac assumption'
+    assumptionOpts = initTacOpts assumption'
+
+private
+  open import Tactic.Defaults
+  module Test where
+    test₁ : {A B : Set} → A → B → A
+    test₁ a b = assumption
+
+    test₂ : {A B : Set} → A → B → B
+    test₂ a b = assumption
\ No newline at end of file diff --git a/Tactic.Case.html b/Tactic.Case.html index 8401b93..77deeb0 100644 --- a/Tactic.Case.html +++ b/Tactic.Case.html @@ -53,17 +53,17 @@ b : B test₁ : A × B → A - test₁ x = by (case x assumption') + test₁ x = by (case x assumption') test₂ : A × B → B - test₂ x = by (case x assumption') + test₂ x = by (case x assumption') test₃ : A ⊎ A → A - test₃ x = by (case x assumption') + test₃ x = by (case x assumption') test₄ : TestType → A - test₄ x = by (case x assumption') + test₄ x = by (case x assumption') test₅ : TestType → B - test₅ x = by (case x assumption') + test₅ x = by (case x assumption') \ No newline at end of file diff --git a/Tactic.Constrs.html b/Tactic.Constrs.html index 939dea2..220b4ac 100644 --- a/Tactic.Constrs.html +++ b/Tactic.Constrs.html @@ -84,5 +84,5 @@ test₃ = tryConstrs 2 test₄ : ∀ {a} {A : Set a} {x y : A} → x ≡ y → (1 ≡ 2) ⊎ (x ≡ y) - test₄ h = tryConstrsWith 2 assumption' + test₄ h = tryConstrsWith 2 assumption' \ No newline at end of file diff --git a/Tactic.Intro.html b/Tactic.Intro.html index 3c6fe8f..dcdf929 100644 --- a/Tactic.Intro.html +++ b/Tactic.Intro.html @@ -40,10 +40,10 @@ macro intro→fill : ⦃ TCOptions ⦄ → Tactic - intro→fill = initTac ⦃ defaultTCOptionsI ⦄ $ intro assumption' + intro→fill = initTac ⦃ defaultTCOptionsI ⦄ $ intro assumption' intros→fill : ⦃ TCOptions ⦄ → Tactic - intros→fill = initTac ⦃ defaultTCOptionsI ⦄ $ intros 5 assumption' + intros→fill = initTac ⦃ defaultTCOptionsI ⦄ $ intros 5 assumption' _ : ℕ → ℕ _ = intro→fill diff --git a/Tactic.ReduceDec.html b/Tactic.ReduceDec.html index c516dd8..5100ff2 100644 --- a/Tactic.ReduceDec.html +++ b/Tactic.ReduceDec.html @@ -120,7 +120,7 @@ reduceDecTerm : ReductionOptions → Term → TC (Term × Term) reduceDecTerm r t = do fuel ← getFuel "reduceDec/constrs" - reduceDecTermWith (tryConstrsWith' fuel assumption') r t + reduceDecTermWith (tryConstrsWith' fuel assumption') r t reduceDec' : ReductionOptions → Term → TC Term reduceDec' r t = do diff --git a/typecheck.time b/typecheck.time index 1592242..b25a7a3 100644 --- a/typecheck.time +++ b/typecheck.time @@ -1,17 +1,17 @@ -TOTAL: 3m20s -Algebra/Function: 0m10s -Meta/Prelude: 1m15s +TOTAL: 3m17s +Algebra/Function: 0m9s +Meta/Prelude: 1m14s Class/MonadError: 0m46s Class/MonadReader: 0m0s -Reflection/Syntax: 0m1s +Reflection/Syntax: 0m0s Reflection/Debug: 0m0s -Class/MonadTC: 0m10s -Reflection/TCI: 0m1s +Class/MonadTC: 0m11s +Reflection/TCI: 0m0s Meta/Init: 0m0s Reflection/Tactic: 0m0s -Reflection/Utils: 0m0s +Reflection/Utils: 0m1s Reflection/Utils/Debug: 0m0s -Class/MonadError/Instances: 0m1s +Class/MonadError/Instances: 0m0s Class/MonadReader/Instances: 0m0s Class/MonadTC/Instances: 0m0s Reflection/Utils/TCI: 0m3s @@ -28,14 +28,14 @@ Tactic/Defaults: 0m0s Tactic/Assumption: 0m0s Tactic/ClauseBuilder: 0m32s Tactic/Case: 0m0s -Tactic/Constrs: 0m1s -Tactic/EquationalReasoning: 0m0s +Tactic/Constrs: 0m0s +Tactic/EquationalReasoning: 0m1s Tactic/Eta: 0m0s Tactic/Intro: 0m1s -Tactic/ReduceDec: 0m1s -Tactic/Derive: 0m0s -Tactic/Derive/TestTypes: 0m2s -Tactic/Derive/DecEq: 0m6s -Tactic/Derive/Show: 0m3s +Tactic/ReduceDec: 0m0s +Tactic/Derive: 0m1s +Tactic/Derive/TestTypes: 0m1s +Tactic/Derive/DecEq: 0m7s +Tactic/Derive/Show: 0m2s Tactic: 0m0s standard-library-meta: 0m0s