Does lean have syntax for declaration of signatures?
I've looked but haven't found any mechanism described in the documentation which allows you to describe a section by it's signature. For example, in the section below the syntax of def requires the right hand side (here sorry)
section
variable A : Type
def ident : A → A := sorry
end
Is there anything like a signature which would allow you to forward declare the contents of a section? Such as in the following made up syntax.
signature
variable A : Type
def ident : A → A
end
The closest i've come using actual syntax is the following,
which declares the proofs twice, the second time for keeping the proof on the right hand side as short as possible.
section
variables A B : Type
def ident' {A : Type} : A → A := (λ x, x)
def mp' {A B : Type}: (A → B) → A → B := (λ f, λ x, f x)
/- Signature-/
def ident : A → A := ident'
def mp : (A → B) → A → B := mp'
end
lean
asked Nov 21 at 3:40
matt
3,87811620
add a comment |
I've looked but haven't found any mechanism described in the documentation which allows you to describe a section by it's signature. For example, in the section below the syntax of def requires the right hand side (here sorry)
section
variable A : Type
def ident : A → A := sorry
end
Is there anything like a signature which would allow you to forward declare the contents of a section? Such as in the following made up syntax.
signature
variable A : Type
def ident : A → A
end
The closest i've come using actual syntax is the following,
which declares the proofs twice, the second time for keeping the proof on the right hand side as short as possible.
section
variables A B : Type
def ident' {A : Type} : A → A := (λ x, x)
def mp' {A B : Type}: (A → B) → A → B := (λ f, λ x, f x)
/- Signature-/
def ident : A → A := ident'
def mp : (A → B) → A → B := mp'
end
lean
asked Nov 21 at 3:40
matt
3,87811620
add a comment |
I've looked but haven't found any mechanism described in the documentation which allows you to describe a section by it's signature. For example, in the section below the syntax of def requires the right hand side (here sorry)
section
variable A : Type
def ident : A → A := sorry
end
Is there anything like a signature which would allow you to forward declare the contents of a section? Such as in the following made up syntax.
signature
variable A : Type
def ident : A → A
end
The closest i've come using actual syntax is the following,
which declares the proofs twice, the second time for keeping the proof on the right hand side as short as possible.
section
variables A B : Type
def ident' {A : Type} : A → A := (λ x, x)
def mp' {A B : Type}: (A → B) → A → B := (λ f, λ x, f x)
/- Signature-/
def ident : A → A := ident'
def mp : (A → B) → A → B := mp'
end
lean
asked Nov 21 at 3:40
matt
3,87811620
I've looked but haven't found any mechanism described in the documentation which allows you to describe a section by it's signature. For example, in the section below the syntax of def requires the right hand side (here sorry)
section
variable A : Type
def ident : A → A := sorry
end
Is there anything like a signature which would allow you to forward declare the contents of a section? Such as in the following made up syntax.
signature
variable A : Type
def ident : A → A
end
The closest i've come using actual syntax is the following,
which declares the proofs twice, the second time for keeping the proof on the right hand side as short as possible.
section
variables A B : Type
def ident' {A : Type} : A → A := (λ x, x)
def mp' {A B : Type}: (A → B) → A → B := (λ f, λ x, f x)
/- Signature-/
def ident : A → A := ident'
def mp : (A → B) → A → B := mp'
end
lean
lean
asked Nov 21 at 3:40
matt
3,87811620
asked Nov 21 at 3:40
matt
3,87811620
asked Nov 21 at 3:40
matt
3,87811620
asked Nov 21 at 3:40
matt
3,87811620
asked Nov 21 at 3:40
matt
3,87811620
3,87811620
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
No, forward declarations are not allowed in general. Lean, like most other ITPs, relies on the order of declarations for termination checking. Forward declarations would allow you to introduce arbitrary mutual recursion, which Lean 3 only accepts in a clearly delimited context:
mutual def even, odd
with even : nat → bool
| 0 := tt
| (a+1) := odd a
with odd : nat → bool
| 0 := ff
| (a+1) := even a
(from Theorem Proving in Lean)
answered Nov 21 at 8:22
Sebastian Ullrich
1,02969
Thanks for confirming, while I don't really want forward declarations, e.g. just for organization/grep, it is good to know why. I was just hoping there was something like the tutch requirements file, tutch req file which doesn't forward declare but just type checks against the requirements.
– matt
Nov 22 at 0:33
I see. I'm afraid it's just not a style popular in ITPs Lean was inspired by (Coq, Agda, Isabelle, ...).
– Sebastian Ullrich
Nov 23 at 9:11
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
StackExchange.using("externalEditor", function () {
StackExchange.using("snippets", function () {
StackExchange.snippets.init();
});
});
}, "code-snippets");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "1"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53404943%2fdoes-lean-have-syntax-for-declaration-of-signatures%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
No, forward declarations are not allowed in general. Lean, like most other ITPs, relies on the order of declarations for termination checking. Forward declarations would allow you to introduce arbitrary mutual recursion, which Lean 3 only accepts in a clearly delimited context:
mutual def even, odd
with even : nat → bool
| 0 := tt
| (a+1) := odd a
with odd : nat → bool
| 0 := ff
| (a+1) := even a
(from Theorem Proving in Lean)
answered Nov 21 at 8:22
Sebastian Ullrich
1,02969
Thanks for confirming, while I don't really want forward declarations, e.g. just for organization/grep, it is good to know why. I was just hoping there was something like the tutch requirements file, tutch req file which doesn't forward declare but just type checks against the requirements.
– matt
Nov 22 at 0:33
I see. I'm afraid it's just not a style popular in ITPs Lean was inspired by (Coq, Agda, Isabelle, ...).
– Sebastian Ullrich
Nov 23 at 9:11
add a comment |
No, forward declarations are not allowed in general. Lean, like most other ITPs, relies on the order of declarations for termination checking. Forward declarations would allow you to introduce arbitrary mutual recursion, which Lean 3 only accepts in a clearly delimited context:
mutual def even, odd
with even : nat → bool
| 0 := tt
| (a+1) := odd a
with odd : nat → bool
| 0 := ff
| (a+1) := even a
(from Theorem Proving in Lean)
answered Nov 21 at 8:22
Sebastian Ullrich
1,02969
Thanks for confirming, while I don't really want forward declarations, e.g. just for organization/grep, it is good to know why. I was just hoping there was something like the tutch requirements file, tutch req file which doesn't forward declare but just type checks against the requirements.
– matt
Nov 22 at 0:33
I see. I'm afraid it's just not a style popular in ITPs Lean was inspired by (Coq, Agda, Isabelle, ...).
– Sebastian Ullrich
Nov 23 at 9:11
add a comment |
No, forward declarations are not allowed in general. Lean, like most other ITPs, relies on the order of declarations for termination checking. Forward declarations would allow you to introduce arbitrary mutual recursion, which Lean 3 only accepts in a clearly delimited context:
mutual def even, odd
with even : nat → bool
| 0 := tt
| (a+1) := odd a
with odd : nat → bool
| 0 := ff
| (a+1) := even a
(from Theorem Proving in Lean)
answered Nov 21 at 8:22
Sebastian Ullrich
1,02969
No, forward declarations are not allowed in general. Lean, like most other ITPs, relies on the order of declarations for termination checking. Forward declarations would allow you to introduce arbitrary mutual recursion, which Lean 3 only accepts in a clearly delimited context:
mutual def even, odd
with even : nat → bool
| 0 := tt
| (a+1) := odd a
with odd : nat → bool
| 0 := ff
| (a+1) := even a
(from Theorem Proving in Lean)
answered Nov 21 at 8:22
Sebastian Ullrich
1,02969
answered Nov 21 at 8:22
Sebastian Ullrich
1,02969
answered Nov 21 at 8:22
Sebastian Ullrich
1,02969
answered Nov 21 at 8:22
Sebastian Ullrich
1,02969
1,02969
Thanks for confirming, while I don't really want forward declarations, e.g. just for organization/grep, it is good to know why. I was just hoping there was something like the tutch requirements file, tutch req file which doesn't forward declare but just type checks against the requirements.
– matt
Nov 22 at 0:33
I see. I'm afraid it's just not a style popular in ITPs Lean was inspired by (Coq, Agda, Isabelle, ...).
– Sebastian Ullrich
Nov 23 at 9:11
add a comment |
Thanks for confirming, while I don't really want forward declarations, e.g. just for organization/grep, it is good to know why. I was just hoping there was something like the tutch requirements file, tutch req file which doesn't forward declare but just type checks against the requirements.
– matt
Nov 22 at 0:33
I see. I'm afraid it's just not a style popular in ITPs Lean was inspired by (Coq, Agda, Isabelle, ...).
– Sebastian Ullrich
Nov 23 at 9:11
Thanks for confirming, while I don't really want forward declarations, e.g. just for organization/grep, it is good to know why. I was just hoping there was something like the tutch requirements file, tutch req file which doesn't forward declare but just type checks against the requirements.
– matt
Nov 22 at 0:33
Thanks for confirming, while I don't really want forward declarations, e.g. just for organization/grep, it is good to know why. I was just hoping there was something like the tutch requirements file, tutch req file which doesn't forward declare but just type checks against the requirements.
– matt
Nov 22 at 0:33
I see. I'm afraid it's just not a style popular in ITPs Lean was inspired by (Coq, Agda, Isabelle, ...).
– Sebastian Ullrich
Nov 23 at 9:11
I see. I'm afraid it's just not a style popular in ITPs Lean was inspired by (Coq, Agda, Isabelle, ...).
– Sebastian Ullrich
Nov 23 at 9:11
add a comment |
Thanks for contributing an answer to Stack Overflow!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Some of your past answers have not been well-received, and you're in danger of being blocked from answering.
Please pay close attention to the following guidance:
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fstackoverflow.com%2fquestions%2f53404943%2fdoes-lean-have-syntax-for-declaration-of-signatures%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
