1e6b3614ab
@Kha, we now support variable/constant shadowing in patterns.
A constant may occur in a pattern if it is a constructor or tagged with
the new [pattern] attribute. In the standard library, I have tagged
'add', 'zero', 'one', 'bit0', 'bit1' and 'rfl' with this new attribute.
BTW, arbitrary constants and variables may occur nested in type ascriptions and
inaccessible terms.
Here is an example:
meta_definition tactic_result_to_string {A : Type} : tactic_result A → string
| (success a s) := to_string a
| (exception ⌞A⌟ e s) := "Exception: " ++ to_string (e ())
I had to use the inaccessible ⌞A⌟ in the example above, otherwise, we would be shadowing the parameter
{A : Type}, and we would get a type error.
The new validation is performed at to_pattern_fn (parser.cpp).
73 lines
1.9 KiB
Text
73 lines
1.9 KiB
Text
/-
|
||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura
|
||
-/
|
||
prelude
|
||
import init.to_string init.prod
|
||
|
||
inductive ordering :=
|
||
| lt | eq | gt
|
||
|
||
open ordering
|
||
|
||
definition ordering.has_to_string [instance] : has_to_string ordering :=
|
||
has_to_string.mk (λ s, match s with | ordering.lt := "lt" | ordering.eq := "eq" | ordering.gt := "gt" end)
|
||
|
||
structure has_ordering [class] (A : Type) :=
|
||
(cmp : A → A → ordering)
|
||
|
||
definition nat.cmp (a b : nat) : ordering :=
|
||
if a < b then lt
|
||
else if a = b then eq
|
||
else gt
|
||
|
||
definition nat_has_ordering [instance] : has_ordering nat :=
|
||
has_ordering.mk nat.cmp
|
||
|
||
section
|
||
open prod
|
||
|
||
variables {A B : Type} [has_ordering A] [has_ordering B]
|
||
|
||
definition prod.cmp : A × B → A × B → ordering
|
||
| (a₁, b₁) (a₂, b₂) :=
|
||
match has_ordering.cmp a₁ a₂ with
|
||
| ordering.lt := lt
|
||
| ordering.eq := has_ordering.cmp b₁ b₂
|
||
| ordering.gt := gt
|
||
end
|
||
|
||
definition prod_has_ordering [instance] {A B : Type} [has_ordering A] [has_ordering B] : has_ordering (A × B) :=
|
||
has_ordering.mk prod.cmp
|
||
end
|
||
|
||
section
|
||
open sum
|
||
|
||
variables {A B : Type} [has_ordering A] [has_ordering B]
|
||
|
||
definition sum.cmp : sum A B → sum A B → ordering
|
||
| (inl a₁) (inl a₂) := has_ordering.cmp a₁ a₂
|
||
| (inr b₁) (inr b₂) := has_ordering.cmp b₁ b₂
|
||
| (inl a₁) (inr b₂) := lt
|
||
| (inr b₁) (inl a₂) := gt
|
||
|
||
definition sum_has_ordering [instance] {A B : Type} [has_ordering A] [has_ordering B] : has_ordering (sum A B) :=
|
||
has_ordering.mk sum.cmp
|
||
end
|
||
|
||
section
|
||
open option
|
||
|
||
variables {A : Type} [has_ordering A]
|
||
|
||
definition option.cmp : option A → option A → ordering
|
||
| (some a₁) (some a₂) := has_ordering.cmp a₁ a₂
|
||
| (some a₁) none := gt
|
||
| none (some a₂) := lt
|
||
| none none := eq
|
||
|
||
definition option_has_ordering [instance] {A : Type} [has_ordering A] : has_ordering (option A) :=
|
||
has_ordering.mk option.cmp
|
||
end
|