{-# OPTIONS --safe --cubical-compatible --no-sized-types --no-guardedness #-}

module SemanticExplanation.Reflection.Reduce where

open import SemanticExplanation.Base
open import Agda.Builtin.Sigma using (_,_)
open import Agda.Builtin.Reflection
  using (Name ; Term ; TC ; reduce ; withReduceDefs)

-- `reduce` exposes weak-head structure.  The enclosing whitelist makes every
-- definitional unfolding an explicit domain decision.
reduceWhnfWith : List Name → Term → TC Term
reduceWhnfWith allowed term = withReduceDefs (true , allowed) (reduce term)