{-# OPTIONS --safe --without-K #-}
module Tactic.Defaults where
 
open import Meta.Prelude
 
open import Class.MonadTC
open import Reflection.Debug
 
-- There should only ever be one instance, with this being convenient
-- to tweak all at once
instance
  defaultTCOptionsI = record
    { debug = record defaultDebugOptions
      { prefix = '┃' -- ┃⎸
      ; filter = Filter.⊥
      }
    ; fuel  = ("reduceDec/constrs" , ) ∷ []
    }