docs: added library documentation for Elab
#3635
Conversation
|
|
||
| ||| `%search` | ||
| ISearch : FC -> (depth : Nat) -> TTImp | ||
| IAlternative : FC -> AltType -> List TTImp -> TTImp |
There was a problem hiding this comment.
This operation is for expression that tries to typecheck expression in the list according to the given AltType and return either one of them, or default one (if present in the AltType), or fails
There was a problem hiding this comment.
Because I'm not familiar with this, I'm just going to copy paste your description if that's alright with you
| ||| A function type | ||
| ||| @ Count the multiplicity of the arguement | ||
| ||| @ PiInfo If the arguement is implicit, explicit, auto implicit or a default implicit | ||
| ||| @ (Maybe Name) the optional index, such as `x` in `(x : Type) -> Type` | ||
| ||| @ argTy the type of the argument | ||
| ||| @ retTy the return type |
There was a problem hiding this comment.
I really like the style of tacit docstrings you added in the second half of TTImp, also mentioning expressions in the surface langauge that correspond to constructors of TTImp. I think this style should be appropriate also for these constructors in the beginning of TTImp.
| ||| A function type, of the form `(mult binder : argTy) -> retTy`, with implicitness determined by `info` | ||
| IPi : FC -> (mult : Count) -> (info : PiInfo TTImp) -> (binder : Maybe Name) -> |
There was a problem hiding this comment.
Could you please change info to piinfo, because info seems to be too generic
| ||| A view in a `with` rule | ||
| IWithApp : FC -> TTImp -> TTImp -> TTImp |
There was a problem hiding this comment.
This is not a view. View with with-rule is done through appropriate WithClause consturctor of the Clause data type. IWithApp is an application in form of f | arg which can be used only inside with-clauses.
|
|
||
| ||| `%search` | ||
| ISearch : FC -> (depth : Nat) -> TTImp | ||
| IAlternative : FC -> AltType -> List TTImp -> TTImp |
| ||| Any implicit bindings in the scope should be bound here, using | ||
| ||| the given binder | ||
| IBindHere : FC -> BindMode -> TTImp -> TTImp |
There was a problem hiding this comment.
I'd say "A bound for implicit bindings to be automatically bound using the given bind mode"
| ||| The delay type, `Delay t` | ||
| IDelayed : FC -> LazyReason -> TTImp -> TTImp |
There was a problem hiding this comment.
Delay types are Lazy and Inf (depending on the LazyReason argument). Delay is a constructor of a lazy value, it is of type a -> Lazy a or a -> Inf a depending on the context
| INamespace : FC -> Namespace -> (decls : List Decl) -> Decl | ||
| ||| A transformation declaration | ||
| ITransform : FC -> Name -> TTImp -> TTImp -> Decl | ||
| ||| A top-level elaboration run |
There was a problem hiding this comment.
| ||| A top-level elaboration run | |
| ||| A top-level elaborator script run, `%runElab` |
| (totality : Maybe TotalReq) -> (rec : Record) -> Decl | ||
| ||| A namespace declaration, `namespace ns where decls` | ||
| INamespace : FC -> Namespace -> (decls : List Decl) -> Decl | ||
| ||| A transformation declaration |
There was a problem hiding this comment.
| ||| A transformation declaration | |
| ||| A transformation rule declaration |
| WithDefault Visibility Private -> | ||
| Maybe TotalReq -> Record -> Decl | ||
| (ns : Maybe String) -> | ||
| (vis : WithDefault Visibility Private) -> |
There was a problem hiding this comment.
Is there any need for names here? I suppose, their types are self expanatory and they are not used on the documentation either, so these names, I think, just clutter reading. What do you think?
| ||| A type ascription, `a : b`. | ||
| ||| Called a claim because of Curry Howard, the statement `x : p` is equivalent to `x` is a proof of `p`. | ||
| IClaim : (claim : WithFC IClaimData) -> Decl | ||
| ||| A data declaration |
There was a problem hiding this comment.
| ||| A data declaration | |
| ||| A data type declaration |
| IData : FC -> (vis : WithDefault Visibility Private) -> Maybe TotalReq -> (cons : Data) -> Decl | ||
| ||| A function definition by its clauses | ||
| IDef : FC -> (f : Name) -> (cls : List Clause) -> Decl | ||
| ||| A parameter block |
There was a problem hiding this comment.
I'd suggest giving an example here, something like
| ||| A parameter block | |
| ||| A parameters block, e.g. `parameters {0 m : _} {auto _ : Monad m} (level : Nat) |
2 participants
Description
Added documentation for
Language.ReflectionSelf-check