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

chore: renamed constant to opaque

Browse source
This commit is contained in:
Yuri de Wit 2022-07-13 10:04:03 -03:00 • committed by Leonardo de Moura
parent aeeaaa6efc
commit dc8e404d15
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
doc/declarations.md
View file

@ -74,7 +74,7 @@ Lean provides ways of adding new objects to the environment. The following provi
* ``axiom c : α`` : declare a constant named ``c`` of type ``α``, it is postulating that `α` is not an empty type.
* ``def c : α := v`` : defines ``c`` to denote ``v``, which should have type ``α``.
* ``theorem c : p := v`` : similar to ``def``, but intended to be used when ``p`` is a proposition.
* ``constant c : α (:= v)?`` : declares a opaque constant named ``c`` of type ``α``, the optional value `v` is must have type `α`
* ``opaque c : α (:= v)?`` : declares a opaque constant named ``c`` of type ``α``, the optional value `v` is must have type `α`
and can be viewed as a certificate that ``α`` is not an empty type. If the value is not provided, Lean tries to find one
using a proceture based on type class resolution. The value `v` is hidden from the type checker. You can assume that
Lean "forgets" `v` after type checking this kind of declaration.
@ -89,8 +89,8 @@ Any of ``def``, ``theorem``, ``axiom``, or ``example`` can take a list of argume
is interpreted as ``def foo : (a : α) → β := fun a : α => t``. Similarly, a theorem ``theorem foo (a : α) : p := t`` is interpreted as ``theorem foo : ∀ a : α, p := fun a : α => t``.
```lean
constant c : Nat
constant d : Nat
opaque c : Nat
opaque d : Nat
axiom cd_eq : c = d
def foo : Nat := 5