@@ -139,6 +139,7 @@ data Elab : Type -> Type where
139139 prim__Compute : Elab ()
140140 prim__Normalise : (List (TTName, Binder TT)) -> TT -> Elab TT
141141 prim__Whnf : TT -> Elab TT
142+ prim__Converts : (List (TTName, Binder TT)) -> TT -> TT -> Elab ()
142143
143144 prim__DeclareType : TyDecl -> Elab ()
144145 prim__DefineFunction : FunDefn -> Elab ()
@@ -373,6 +374,21 @@ namespace Tactics
373374 whnf : (term : TT) -> Elab TT
374375 whnf term = prim__Whnf term
375376
377+ ||| Check that two terms are convertable in the current context and environment
378+ |||
379+ ||| @ env a lexical environment to compare the terms in (see `getEnv`)
380+ ||| @ term1 the first term to convert
381+ ||| @ term2 the second term to convert
382+ convertsInEnv : (env : List (TTName, Binder TT)) -> (term1, term2 : TT) -> Elab ()
383+ convertsInEnv env term1 term2 = prim__Converts env term1 term2
384+
385+ ||| Check that two terms are convertable in the current context and environment
386+ |||
387+ ||| @ term1 the first term to convert
388+ ||| @ term2 the second term to convert
389+ converts : (term1, term2 : TT) -> Elab ()
390+ converts term1 term2 = convertsInEnv !getEnv term1 term2
391+
376392 ||| Find the source context for the elaboration script
377393 getSourceLocation : Elab SourceLocation
378394 getSourceLocation = prim__SourceLocation