Mixing
Less then function
I am passing through coq course "Logical Foundations". Solving problem:
Having less or equal function:
Fixpoint leb (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => leb n' m'
end
end.
create "less then" function:
Definition blt_nat (n m : nat) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
As far as I understand it should work like this:
if (n == m)
return false
else
return (leb n m)
I created this:
Definition blt_nat (n m : nat) : bool
match n with
| m => false
| _ => leb n m
end.
But it doesn't work - outputs: "Error: This clause is redundant." for the line:
| _ => leb n m
Please, help.
coq logical-foundations
asked Dec 31 '18 at 14:11
user4035user4035
15k64068
add a comment |
I am passing through coq course "Logical Foundations". Solving problem:
Having less or equal function:
Fixpoint leb (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => leb n' m'
end
end.
create "less then" function:
Definition blt_nat (n m : nat) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
As far as I understand it should work like this:
if (n == m)
return false
else
return (leb n m)
I created this:
Definition blt_nat (n m : nat) : bool
match n with
| m => false
| _ => leb n m
end.
But it doesn't work - outputs: "Error: This clause is redundant." for the line:
| _ => leb n m
Please, help.
coq logical-foundations
asked Dec 31 '18 at 14:11
user4035user4035
15k64068
4
I'm not experienced withcoqbut I suspect the first case| m => ...doesn't match onm, but matches on any value and calls that valuem(overriding the originalm). This might be helpful: stackoverflow.com/a/46384468
– Aurel Bílý
Dec 31 '18 at 14:19
add a comment |
I am passing through coq course "Logical Foundations". Solving problem:
Having less or equal function:
Fixpoint leb (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => leb n' m'
end
end.
create "less then" function:
Definition blt_nat (n m : nat) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
As far as I understand it should work like this:
if (n == m)
return false
else
return (leb n m)
I created this:
Definition blt_nat (n m : nat) : bool
match n with
| m => false
| _ => leb n m
end.
But it doesn't work - outputs: "Error: This clause is redundant." for the line:
| _ => leb n m
Please, help.
coq logical-foundations
asked Dec 31 '18 at 14:11
user4035user4035
15k64068
I am passing through coq course "Logical Foundations". Solving problem:
Having less or equal function:
Fixpoint leb (n m : nat) : bool :=
match n with
| O => true
| S n' =>
match m with
| O => false
| S m' => leb n' m'
end
end.
create "less then" function:
Definition blt_nat (n m : nat) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
As far as I understand it should work like this:
if (n == m)
return false
else
return (leb n m)
I created this:
Definition blt_nat (n m : nat) : bool
match n with
| m => false
| _ => leb n m
end.
But it doesn't work - outputs: "Error: This clause is redundant." for the line:
| _ => leb n m
Please, help.
coq logical-foundations
coq logical-foundations
asked Dec 31 '18 at 14:11
user4035user4035
15k64068
asked Dec 31 '18 at 14:11
user4035user4035
15k64068
edited Feb 14 at 12:12
user4035
asked Dec 31 '18 at 14:11
user4035user4035
15k64068
asked Dec 31 '18 at 14:11
user4035user4035
15k64068
asked Dec 31 '18 at 14:11
user4035user4035
15k64068
15k64068
4
I'm not experienced withcoqbut I suspect the first case| m => ...doesn't match onm, but matches on any value and calls that valuem(overriding the originalm). This might be helpful: stackoverflow.com/a/46384468
– Aurel Bílý
Dec 31 '18 at 14:19
add a comment |
4
I'm not experienced withcoqbut I suspect the first case| m => ...doesn't match onm, but matches on any value and calls that valuem(overriding the originalm). This might be helpful: stackoverflow.com/a/46384468
– Aurel Bílý
Dec 31 '18 at 14:19
4
4
I'm not experienced with
coq but I suspect the first case | m => ... doesn't match on m, but matches on any value and calls that value m (overriding the original m). This might be helpful: stackoverflow.com/a/46384468– Aurel Bílý
Dec 31 '18 at 14:19
I'm not experienced with
coq but I suspect the first case | m => ... doesn't match on m, but matches on any value and calls that value m (overriding the original m). This might be helpful: stackoverflow.com/a/46384468– Aurel Bílý
Dec 31 '18 at 14:19
add a comment |
1 Answer
1
active
oldest
votes
By using match ... with...end, we can just check the constructors of a particular datatype and find out how it is built based on its constructors. So you cannot do matching a datatype of nat with another datatype of nat. You can find other examples in here.
Definition blt_nat (n m : nat) : bool :=
match m with
| 0 => false
| S m' => leb n m'
end.
edited Jan 1 at 8:02
user4035
15k64068
answered Jan 1 at 6:26
Tom And.Tom And.
1006
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%2f53988404%2fless-then-function%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
By using match ... with...end, we can just check the constructors of a particular datatype and find out how it is built based on its constructors. So you cannot do matching a datatype of nat with another datatype of nat. You can find other examples in here.
Definition blt_nat (n m : nat) : bool :=
match m with
| 0 => false
| S m' => leb n m'
end.
edited Jan 1 at 8:02
user4035
15k64068
answered Jan 1 at 6:26
Tom And.Tom And.
1006
add a comment |
By using match ... with...end, we can just check the constructors of a particular datatype and find out how it is built based on its constructors. So you cannot do matching a datatype of nat with another datatype of nat. You can find other examples in here.
Definition blt_nat (n m : nat) : bool :=
match m with
| 0 => false
| S m' => leb n m'
end.
edited Jan 1 at 8:02
user4035
15k64068
answered Jan 1 at 6:26
Tom And.Tom And.
1006
add a comment |
By using match ... with...end, we can just check the constructors of a particular datatype and find out how it is built based on its constructors. So you cannot do matching a datatype of nat with another datatype of nat. You can find other examples in here.
Definition blt_nat (n m : nat) : bool :=
match m with
| 0 => false
| S m' => leb n m'
end.
edited Jan 1 at 8:02
user4035
15k64068
answered Jan 1 at 6:26
Tom And.Tom And.
1006
By using match ... with...end, we can just check the constructors of a particular datatype and find out how it is built based on its constructors. So you cannot do matching a datatype of nat with another datatype of nat. You can find other examples in here.
Definition blt_nat (n m : nat) : bool :=
match m with
| 0 => false
| S m' => leb n m'
end.
edited Jan 1 at 8:02
user4035
15k64068
answered Jan 1 at 6:26
Tom And.Tom And.
1006
edited Jan 1 at 8:02
user4035
15k64068
edited Jan 1 at 8:02
user4035
15k64068
edited Jan 1 at 8:02
user4035
15k64068
15k64068
answered Jan 1 at 6:26
Tom And.Tom And.
1006
answered Jan 1 at 6:26
Tom And.Tom And.
1006
answered Jan 1 at 6:26
Tom And.Tom And.
1006
1006
add a comment |
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.
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%2f53988404%2fless-then-function%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
4
I'm not experienced with
coqbut I suspect the first case| m => ...doesn't match onm, but matches on any value and calls that valuem(overriding the originalm). This might be helpful: stackoverflow.com/a/46384468– Aurel Bílý
Dec 31 '18 at 14:19