5045dae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added tactic for case analysis.

5045daeAhmad Salim Al-Sibahi12 years ago

libs/base/Language/Reflection.idr+2

compare with master

unifiedsplit

@@ -194,6 +194,8 @@ data Tactic = Try Tactic Tactic

194 -- ^ rewrite using the reflected rep. of a equality proof

195 | Induction TT

196 -- ^ do induction on the particular expression

197+ | Case TT

198+ -- ^ do case analysis on particular expression

197 | LetTac TTName TT

199 | LetTac TTName TT

198 -- ^ name a reflected term

200 -- ^ name a reflected term

199 | LetTacTy TTName TT TT

201 | LetTacTy TTName TT TT

libs/prelude/Prelude/Bool.idr+1−1

@@ -5,7 +5,7 @@ import Builtins

5import Prelude.Uninhabited

7||| Boolean Data Type

8−data Bool = False | True

8+%case data Bool = False | True

10||| The underlying implementation of the if ... then ... else ... syntax

11||| @ b the condition on the if

src/Idris/AbsSyntaxTree.hs+4−2

@@ -484,8 +484,9 @@ dictionary = elem Dictionary

484

485

486-- | Data declaration options

487−data DataOpt = Codata -- Set if the the data-type is coinductive

487+data DataOpt = Codata -- ^ Set if the the data-type is coinductive

488− | DefaultEliminator -- Set if an eliminator should be generated for data type

488+ | DefaultEliminator -- ^ Set if an eliminator should be generated for data type

489+ | DefaultCaseFun -- ^ Set if a case function should be generated for data type

489 | DataErrRev

490 | DataErrRev

490 deriving (Show, Eq)

491 deriving (Show, Eq)

491

492

@@ -738,6 +739,7 @@ mapPT f t = f (mpt t) where

738data PTactic' t = Intro [Name] | Intros | Focus Name

739data PTactic' t = Intro [Name] | Intros | Focus Name

739 | Refine Name [Bool] | Rewrite t | DoUnify

740 | Refine Name [Bool] | Rewrite t | DoUnify

740 | Induction t

741 | Induction t

742+ | CaseTac t

741 | Equiv t

743 | Equiv t

742 | MatchRefine Name

744 | MatchRefine Name

743 | LetTac Name t | LetTacTy Name t t

745 | LetTac Name t | LetTacTy Name t t

src/Idris/Core/Elaborate.hs+3

@@ -374,6 +374,9 @@ rewrite tm = processTactic' (Rewrite tm)

374induction :: Raw -> Elab' aux ()

375induction tm = processTactic' (Induction tm)

376

377+casetac :: Raw -> Elab' aux ()

378+casetac tm = processTactic' (CaseTac tm)

379+

377equiv :: Raw -> Elab' aux ()

380equiv :: Raw -> Elab' aux ()

378equiv tm = processTactic' (Equiv tm)

381equiv tm = processTactic' (Equiv tm)

379

382

src/Idris/Core/ProofState.hs+14−9

@@ -73,6 +73,7 @@ data Tactic = Attack

73 | ExpandLet Name Term

74 | Rewrite Raw

75 | Induction Raw

76+ | CaseTac Raw

76 | Equiv Raw

77 | Equiv Raw

77 | PatVar Name

78 | PatVar Name

78 | PatBind Name

79 | PatBind Name

@@ -661,13 +662,16 @@ mkP lt l r (Bind n b sc)

661 b { binderTy = ty' }

662 b { binderTy = ty' }

662mkP lt l r x = x

663mkP lt l r x = x

663

664

664−induction :: Raw -> RunTactic

665+casetac :: Raw -> Bool -> RunTactic

665−induction tm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

666+casetac tm induction ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

666 (tmv, tmt) <- lift $ check ctxt env tm

667 (tmv, tmt) <- lift $ check ctxt env tm

667 let tmt' = normalise ctxt env tmt

668 let tmt' = normalise ctxt env tmt

669+ let (tacn, tacstr, tactt) = if induction

670+ then (ElimN, "an eliminator", "induction")

671+ else (CaseN, "a case function", "case analysis")

668 case unApply tmt' of

672 case unApply tmt' of

669 (P _ tnm _, tyargs) -> do

673 (P _ tnm _, tyargs) -> do

670− case lookupTy (SN (ElimN tnm)) ctxt of

674+ case lookupTy (SN (tacn tnm)) ctxt of

671 [elimTy] -> do

675 [elimTy] -> do

672 param_pos <- case lookupMetaInformation tnm ctxt of

676 param_pos <- case lookupMetaInformation tnm ctxt of

673 [DataMI param_pos] -> return param_pos

677 [DataMI param_pos] -> return param_pos

@@ -690,7 +694,7 @@ induction tm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

690 let tmvar = P Bound tmnm tmt'

694 let tmvar = P Bound tmnm tmt'

691 prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)

695 prop <- replaceIndicies indxnames indicies $ Bind tmnm (Lam tmt') (mkP tmvar tmv tmvar t)

692 consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (pterm ps)) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (pterm ps))) consargs)

696 consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (pterm ps)) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (pterm ps))) consargs)

693− let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0)))

697+ let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (tacn tnm)) (TType (UVal 0)))

694 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))

698 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))

695 action (\ps -> ps {holes = holes ps \\ [x]})

699 action (\ps -> ps {holes = holes ps \\ [x]})

696 mapM_ addConsHole (reverse consargs')

700 mapM_ addConsHole (reverse consargs')

@@ -698,9 +702,9 @@ induction tm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

698 (scv, sct) <- lift $ check ctxt env res'

702 (scv, sct) <- lift $ check ctxt env res'

699 let scv' = specialise ctxt env [] scv

703 let scv' = specialise ctxt env [] scv

700 return scv'

704 return scv'

701− [] -> fail $ "Induction needs an eliminator for " ++ show tnm

705+ [] -> fail $ tactt ++ " needs " ++ tacstr ++ " for " ++ show tnm

702− xs -> fail $ "Multiple definitions found when searching for the eliminator of " ++ show tnm

706+ xs -> fail $ "Multiple definitions found when searching for " ++ tacstr ++ "of " ++ show tnm

703− _ -> fail "Unkown type for induction"

707+ _ -> fail $ "Unkown type for " ++ if induction then "induction" else "case analysis"

704 where scname = sMN 0 "scarg"

708 where scname = sMN 0 "scarg"

705 makeConsArg (nm, ty) = P Bound nm ty

709 makeConsArg (nm, ty) = P Bound nm ty

706 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

710 bindConsArgs ((nm, ty):args) v = Bind nm (Hole ty) $ bindConsArgs args v

@@ -714,7 +718,7 @@ induction tm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

714 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)

718 replaceIndicies idnms idxs prop = foldM (\t (idnm, idx) -> do (idxv, idxt) <- lift $ check ctxt env (forget idx)

715 let var = P Bound idnm idxt

719 let var = P Bound idnm idxt

716 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs

720 return $ Bind idnm (Lam idxt) (mkP var idxv var t)) prop $ zip idnms idxs

717−induction tm ctxt env _ = do fail "Can't do induction here"

721+induction tm induction ctxt env _ = do fail "Can't do induction here"

718

722

719

723

720equiv :: Raw -> RunTactic

724equiv :: Raw -> RunTactic

@@ -992,7 +996,8 @@ process t h = tactic (Just h) (mktac t)

992 mktac (LetBind n t v) = letbind n t v

996 mktac (LetBind n t v) = letbind n t v

993 mktac (ExpandLet n b) = expandLet n b

997 mktac (ExpandLet n b) = expandLet n b

994 mktac (Rewrite t) = rewrite t

998 mktac (Rewrite t) = rewrite t

995− mktac (Induction t) = induction t

999+ mktac (Induction t) = casetac t True

1000+ mktac (CaseTac t) = casetac t False

996 mktac (Equiv t) = equiv t

1001 mktac (Equiv t) = equiv t

997 mktac (PatVar n) = patvar n

1002 mktac (PatVar n) = patvar n

998 mktac (PatBind n) = patbind n

1003 mktac (PatBind n) = patbind n

src/Idris/ElabDecls.hs+17−11

@@ -283,7 +283,10 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

283

284 -- create an eliminator

285 when (DefaultEliminator `elem` opts) $

286+ evalStateT (elabCaseFun True params n t dcons info) Map.empty

287+ -- create a case function

288+ when (DefaultCaseFun `elem` opts) $

286− evalStateT (elabEliminator params n t dcons info) Map.empty

289+ evalStateT (elabCaseFun False params n t dcons info) Map.empty

287 where

290 where

288 setDetaggable :: Name -> Idris ()

291 setDetaggable :: Name -> Idris ()

289 setDetaggable n = do

292 setDetaggable n = do

@@ -369,11 +372,13 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

369type EliminatorState = StateT (Map.Map String Int) Idris

372type EliminatorState = StateT (Map.Map String Int) Idris

370

373

371-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

374-- TODO: Rewrite everything to use idris_implicits instead of manual splitting (or in TT)

375+-- FIXME: Many things have name starting with elim internally since this was the only purpose in the first edition of the function

376+-- rename to caseFun to match updated intend

372−elabEliminator :: [Int] -> Name -> PTerm ->

377+elabCaseFun :: Bool -> [Int] -> Name -> PTerm ->

373 [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->

378 [(Docstring, [(Name, Docstring)], Name, PTerm, FC, [Name])] ->

374 ElabInfo -> EliminatorState ()

379 ElabInfo -> EliminatorState ()

375−elabEliminator paramPos n ty cons info = do

380+elabCaseFun ind paramPos n ty cons info = do

376− elimLog $ "Elaborating eliminator"

381+ elimLog $ "Elaborating case function"

377 put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

382 put (Map.fromList $ zip (concatMap (\(_, p, _, ty, _, _) -> (map show $ boundNamesIn ty) ++ map (show . fst) p) cons ++ (map show $ boundNamesIn ty)) (repeat 0))

378 let (cnstrs, _) = splitPi ty

383 let (cnstrs, _) = splitPi ty

379 let (splittedTy@(pms, idxs)) = splitPms cnstrs

384 let (splittedTy@(pms, idxs)) = splitPms cnstrs

@@ -381,7 +386,8 @@ elabEliminator paramPos n ty cons info = do

381 motiveIdxs <- namePis False idxs

386 motiveIdxs <- namePis False idxs

382 let motive = mkMotive n paramPos generalParams motiveIdxs

387 let motive = mkMotive n paramPos generalParams motiveIdxs

383 consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do

388 consTerms <- mapM (\(c@(_, _, cnm, _, _, _)) -> do

389+ let casefunt = if ind then "elim_" else "case_"

384− name <- freshName $ "elim_" ++ simpleName cnm

390+ name <- freshName $ casefunt ++ simpleName cnm

385 consTerm <- extractConsTerm c generalParams

391 consTerm <- extractConsTerm c generalParams

386 return (name, expl, consTerm)) cons

392 return (name, expl, consTerm)) cons

387 scrutineeIdxs <- namePis False idxs

393 scrutineeIdxs <- namePis False idxs

@@ -392,11 +398,11 @@ elabEliminator paramPos n ty cons info = do

392 let clauseConsElimArgs = map getPiName consTerms

398 let clauseConsElimArgs = map getPiName consTerms

393 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

399 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

394 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

400 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'

395− let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy

401+ let elimSig = "-- case function signature: " ++ showTmImpls eliminatorTy

396 elimLog elimSig

402 elimLog elimSig

397 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

403 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

398 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

404 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

399− elimLog $ "-- eliminator definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

405+ elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef

400 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

406 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

401 -- Do not elaborate clauses if there aren't any

407 -- Do not elaborate clauses if there aren't any

402 case eliminatorClauses of

408 case eliminatorClauses of

@@ -406,10 +412,10 @@ elabEliminator paramPos n ty cons info = do

406 elimLog s = State.lift (logLvl 2 s)

412 elimLog s = State.lift (logLvl 2 s)

407

413

408 elimFC :: FC

414 elimFC :: FC

409− elimFC = fileFC "(eliminator)"

415+ elimFC = fileFC "(casefun)"

410

416

411 elimDeclName :: Name

417 elimDeclName :: Name

412− elimDeclName = SN $ ElimN n

418+ elimDeclName = if ind then SN . ElimN $ n else SN . CaseN $ n

413

419

414 applyNS :: Name -> [String] -> Name

420 applyNS :: Name -> [String] -> Name

415 applyNS n [] = n

421 applyNS n [] = n

@@ -560,7 +566,7 @@ elabEliminator paramPos n ty cons info = do

560 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

566 implidxs <- implicitIndexes (doc, cnm, ty, fc, fs)

561 consArgs <- namePis False args

567 consArgs <- namePis False args

562 let recArgs = findRecArgs consArgs

568 let recArgs = findRecArgs consArgs

563− let recMotives = map applyRecMotive recArgs

569+ let recMotives = if ind then map applyRecMotive recArgs else []

564 let (_, consIdxs) = splitArgPms resTy

570 let (_, consIdxs) = splitArgPms resTy

565 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))

571 return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))

566 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)

572 where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)

@@ -600,7 +606,7 @@ elabEliminator paramPos n ty cons info = do

600 consArgs <- namePis False args

606 consArgs <- namePis False args

601 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

607 let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])

602 let recArgs = findRecArgs consArgs

608 let recArgs = findRecArgs consArgs

603− let recElims = map applyRecElim recArgs

609+ let recElims = if ind then map applyRecElim recArgs else []

604 let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)

610 let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)

605 return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []

611 return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []

606 where applyRecElim :: (Name, Plicity, PTerm) -> PArg

612 where applyRecElim :: (Name, Plicity, PTerm) -> PArg

src/Idris/ElabTerm.hs+21−14

@@ -956,6 +956,24 @@ collectDeferred top (Bind n b t) = do b' <- cdb b

956collectDeferred top (App f a) = liftM2 App (collectDeferred top f) (collectDeferred top a)

957collectDeferred top t = return t

958

959+case_ :: Bool -> Bool -> IState -> Name -> PTerm -> ElabD ()

960+case_ ind autoSolve ist fn tm = do

961+ attack

962+ tyn <- getNameFrom (sMN 0 "ity")

963+ claim tyn RType

964+ valn <- getNameFrom (sMN 0 "ival")

965+ claim valn (Var tyn)

966+ letn <- getNameFrom (sMN 0 "irule")

967+ letbind letn (Var tyn) (Var valn)

968+ focus valn

969+ elab ist toplevel False [] (sMN 0 "tac") tm

970+ env <- get_env

971+ let (Just binding) = lookup letn env

972+ let val = binderVal binding

973+ if ind then induction (forget val)

974+ else casetac (forget val)

975+ when autoSolve solveAll

976+

959-- Running tactics directly

977-- Running tactics directly

960-- if a tactic adds unification problems, return an error

978-- if a tactic adds unification problems, return an error

961

979

@@ -1047,20 +1065,9 @@ runTac autoSolve ist fn tac

1047 rewrite (Var letn)

1065 rewrite (Var letn)

1048 when autoSolve solveAll

1066 when autoSolve solveAll

1049 runT (Induction tm) -- let bind tm, similar to the others

1067 runT (Induction tm) -- let bind tm, similar to the others

1050− = do attack

1068+ = case_ True autoSolve ist fn tm

1051− tyn <- getNameFrom (sMN 0 "ity")

1069+ runT (CaseTac tm)

1052− claim tyn RType

1070+ = case_ False autoSolve ist fn tm

1053− valn <- getNameFrom (sMN 0 "ival")

1054− claim valn (Var tyn)

1055− letn <- getNameFrom (sMN 0 "irule")

1056− letbind letn (Var tyn) (Var valn)

1057− focus valn

1058− elab ist toplevel False [] (sMN 0 "tac") tm

1059− env <- get_env

1060− let (Just binding) = lookup letn env

1061− let val = binderVal binding

1062− induction (forget val)

1063− when autoSolve solveAll

1064 runT (LetTac n tm)

1071 runT (LetTac n tm)

1065 = do attack

1072 = do attack

1066 tyn <- getNameFrom (sMN 0 "letty")

1073 tyn <- getNameFrom (sMN 0 "letty")

src/Idris/IBC.hs+6

@@ -1264,11 +1264,13 @@ instance Binary DataOpt where

1264 Codata -> putWord8 0

1265 DefaultEliminator -> putWord8 1

1266 DataErrRev -> putWord8 2

1267+ DefaultCaseFun -> putWord8 3

1267 get = do i <- getWord8

1268 get = do i <- getWord8

1268 case i of

1269 case i of

1269 0 -> return Codata

1270 0 -> return Codata

1270 1 -> return DefaultEliminator

1271 1 -> return DefaultEliminator

1271 2 -> return DataErrRev

1272 2 -> return DataErrRev

1273+ 3 -> return DefaultCaseFun

1272

1274

1273instance Binary FnOpt where

1275instance Binary FnOpt where

1274 put x

1276 put x

@@ -1968,6 +1970,8 @@ instance (Binary t) => Binary (PTactic' t) where

1968 put x4

1970 put x4

1969 put x5

1971 put x5

1970 DoUnify -> putWord8 22

1972 DoUnify -> putWord8 22

1973+ CaseTac x1 -> do putWord8 23

1974+ put x1

1971 get

1975 get

1972 = do i <- getWord8

1976 = do i <- getWord8

1973 case i of

1977 case i of

@@ -2016,6 +2020,8 @@ instance (Binary t) => Binary (PTactic' t) where

2016 x5 <- get

2020 x5 <- get

2017 return (ProofSearch x1 x2 x3 x4 x5)

2021 return (ProofSearch x1 x2 x3 x4 x5)

2018 22 -> return DoUnify

2022 22 -> return DoUnify

2023+ 23 -> do x1 <- get

2024+ return (CaseTac x1)

2019 _ -> error "Corrupted binary data for PTactic'"

2025 _ -> error "Corrupted binary data for PTactic'"

2020

2026

2021

2027

src/Idris/ParseData.hs+4−3

@@ -79,12 +79,13 @@ dataI :: IdrisParser DataOpts

79dataI = do reserved "data"; return []

80 <|> do reserved "codata"; return [Codata]

82−{- | Parses if a data should not have a default eliminator

82+{- | Parses if a data should not have a default eliminator

83DefaultEliminator ::= 'noelim'?

84 -}

85dataOpts :: DataOpts -> IdrisParser DataOpts

86dataOpts opts

87− = do reserved "%elim"; dataOpts (DefaultEliminator : opts)

87+ = do reserved "%elim"; dataOpts (DefaultEliminator : DefaultCaseFun : opts)

88+ <|> do reserved "%case"; dataOpts (DefaultCaseFun : opts)

88 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

89 <|> do reserved "%error_reverse"; dataOpts (DataErrRev : opts)

89 <|> return opts

90 <|> return opts

90 <?> "data options"

91 <?> "data options"

@@ -129,7 +130,7 @@ data_ syn = do (doc, argDocs, acc, dataOpts) <- try (do

129 let tyn = expandNS syn tyn_in

130 let tyn = expandNS syn tyn_in

130 option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do

131 option (PData doc argDocs syn fc dataOpts (PLaterdecl tyn ty)) (do

131 try (lchar '=') <|> do reserved "where"

132 try (lchar '=') <|> do reserved "where"

132− let kw = (if DefaultEliminator `elem` dataOpts then "" else "%noelim ") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

133+ let kw = (if DefaultEliminator `elem` dataOpts then "%elim" else "") ++ (if Codata `elem` dataOpts then "co" else "") ++ "data "

133 let n = show tyn_in ++ " "

134 let n = show tyn_in ++ " "

134 let s = kw ++ n

135 let s = kw ++ n

135 let as = concat (intersperse " " $ map show args) ++ " "

136 let as = concat (intersperse " " $ map show args) ++ " "

src/Idris/ParseExpr.hs+3

@@ -1184,6 +1184,9 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

1184 <|> do reserved "rewrite"; t <- (indentPropHolds gtProp *> expr syn);

1185 i <- get

1186 return $ Rewrite (desugar syn i t)

1187+ <|> do reserved "case"; t <- (indentPropHolds gtProp *> expr syn);

1188+ i <- get

1189+ return $ CaseTac (desugar syn i t)

1187 <|> do reserved "induction"; t <- (indentPropHolds gtProp *> expr syn);

1190 <|> do reserved "induction"; t <- (indentPropHolds gtProp *> expr syn);

1188 i <- get

1191 i <- get

1189 return $ Induction (desugar syn i t)

1192 return $ Induction (desugar syn i t)