
  0 | module Deriving.DepTyCheck.Gen.ForOneTypeConRhs.Interface
  1 | 
  2 | import public Deriving.DepTyCheck.Gen.ForAllNeededTypes.Interface
  3 | 
  4 | %default total
  5 | 
  6 | ------------------------------------------------------------
  7 | --- Derivation of a generator for constructor's body RHS ---
  8 | ------------------------------------------------------------
  9 | 
 10 | --- Interface ---
 11 | 
 12 | public export
 13 | interface DeriveBodyRhsForCon where
 14 |   consGenExpr : DerivationClosure m => Elaboration m => NamesInfoInTypes => ConsRecs =>
 15 |                 GenSignature -> (con : Con) -> (given : SortedSet $ Fin con.args.length) -> (fuel : TTImp) -> m TTImp
 16 |