Idris2Doc : Idris.Parser.Let

Idris.Parser.Let

(source)
Definitions
record LetBinder : Type
  Totality: total
  Visibility: public export
  Constructor: 
MkLetBinder : RigCount -> PTerm -> PTerm -> PTerm -> List PClause -> LetBinder

  Projections:
  
.letBoundTerm : LetBinder -> PTerm
  
.letBoundType : LetBinder -> PTerm
  
.letPattern : LetBinder -> PTerm
  
.letUnhappy : LetBinder -> List PClause
  
.letUsage : LetBinder -> RigCount
.letUsage : LetBinder -> RigCount
  Totality: total
  Visibility: public export
letUsage : LetBinder -> RigCount
  Totality: total
  Visibility: public export
.letPattern : LetBinder -> PTerm
  Totality: total
  Visibility: public export
letPattern : LetBinder -> PTerm
  Totality: total
  Visibility: public export
.letBoundType : LetBinder -> PTerm
  Totality: total
  Visibility: public export
letBoundType : LetBinder -> PTerm
  Totality: total
  Visibility: public export
.letBoundTerm : LetBinder -> PTerm
  Totality: total
  Visibility: public export
letBoundTerm : LetBinder -> PTerm
  Totality: total
  Visibility: public export
.letUnhappy : LetBinder -> List PClause
  Totality: total
  Visibility: public export
letUnhappy : LetBinder -> List PClause
  Totality: total
  Visibility: public export
LetDecl : Type
  Totality: total
  Visibility: public export
mkLets : OriginDesc -> List1 (WithBounds (Either LetBinder LetDecl)) -> PTerm -> PTerm
  Totality: total
  Visibility: export
mkDoLets : OriginDesc -> List1 (WithBounds (Either LetBinder LetDecl)) -> List PDo
  Totality: total
  Visibility: export