feat: add propper code-gen and support for implicits

Qpf/Macro/Data/Ind.lean

@@ -5,30 +5,16 @@ import Qpf.Qpf.Multivariate.Constructions.DeepThunk
 import Qpf.Macro.Data.Constructors
 import Qpf.Macro.Data.RecForm
 import Qpf.Macro.Data.View
+import Qpf.Macro.ParserUtils
 import Qpf.Macro.Common
 import Qpf.Util.Vec
 
 open Lean.Parser (Parser)
 open Lean Meta Elab.Command Elab.Term Parser.Term
 open Lean.Parser.Tactic (inductionAlt)
 
-
-
 def flattenForArg (n : Name) := Name.str .anonymous $ n.toStringWithSep "_" true
 
-/-- Both `bracketedBinder` and `matchAlts` have optional arguments,
-which cause them to not by recognized as parsers in quotation syntax
-(that is, ``` `(bracketedBinder| ...) ``` does not work).
-To work around this, we define aliases that force the optional argument to it's default value, 
-so that we can write ``` `(bb| ...) ```instead. -/
-abbrev bb            : Parser := bracketedBinder
-abbrev matchAltExprs : Parser := matchAlts
-
-/- Since `bb` and `matchAltExprs` are aliases for `bracketedBinder`, resp. `matchAlts`,
-we can safely coerce syntax of these categories  -/
-instance : Coe (TSyntax ``bb) (TSyntax ``bracketedBinder)      where coe x := ⟨x.raw⟩
-instance : Coe (TSyntax ``matchAltExprs) (TSyntax ``matchAlts) where coe x := ⟨x.raw⟩
-
 section
 variable {m} [Monad m] [MonadQuotation m] [MonadError m] [MonadTrace m] [AddMessageContext m]