max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: update doc string

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-28 06:58:53 -07:00
parent 556358e84c
commit d0d5effcbc
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/Expr.lean
View file

@ -395,7 +395,13 @@ inductive Expr where
| /--
Let-expressions. The field `nonDep` is not currently used, but will be used in the future
by the code generator (and possibly `simp`) to track whether a let-expression is non-dependent
or not. Given an environment, metavariable context, and local context, we say a let-expression
or not.
**IMPORTANT**: This flag is for "local" use only. That is, a module should not "trust" its value for any purpose.
In the intended use-case, the compiler will set this flag, and be responsible for maintaining it.
Other modules may not preserve its value while applying transformations.
Given an environment, metavariable context, and local context, we say a let-expression
`let x : t := v; e` is non-dependent when it is equivalent to `(fun x : t => e) v`.
Here is an example of a dependent let-expression
`let n : Nat := 2; fun (a : Array Nat n) (b : Array Nat 2) => a = b` is type correct, but