From 89e1a404630a00c74c0e2321908cdec6f323b53c Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Sun, 13 Aug 2023 16:52:13 +0300 Subject: [PATCH] [ experim ] Change the rig to 1 --- src/TTImp/ProcessRunElab.idr | 2 +- tests/idris2/reflection021/RunElab0.idr | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/TTImp/ProcessRunElab.idr b/src/TTImp/ProcessRunElab.idr index 9ab2e013588..13a8499a708 100644 --- a/src/TTImp/ProcessRunElab.idr +++ b/src/TTImp/ProcessRunElab.idr @@ -38,5 +38,5 @@ processRunElab eopts nest env fc tm unit <- getCon fc defs (builtin "Unit") exp <- appCon fc defs n [unit] - stm <- checkTerm tidx InExpr (OverrideRig bot :: eopts) nest env tm (gnf env exp) + stm <- checkTerm tidx InExpr (OverrideRig Rig1 :: eopts) nest env tm (gnf env exp) ignore $ elabScript top fc nest env !(nfOpts withAll defs env stm) Nothing diff --git a/tests/idris2/reflection021/RunElab0.idr b/tests/idris2/reflection021/RunElab0.idr index c72996546bc..1ab77b986ef 100644 --- a/tests/idris2/reflection021/RunElab0.idr +++ b/tests/idris2/reflection021/RunElab0.idr @@ -10,4 +10,4 @@ elabScript = pure () x : Unit x = %runElab elabScript -%runElab elabScript +-- %runElab elabScript