90bfd84a07
In the standard library, we should use explicit universe variables for universe polymorphic definitions. Users that want to declare universe polymorphic definitions but do not want to provide universe level parameters should use Type _ or Type*
61 lines
1.8 KiB
Text
61 lines
1.8 KiB
Text
--
|
||
open list nat
|
||
|
||
structure unification_constraint := {A : Type*} (lhs : A) (rhs : A)
|
||
structure unification_hint := (pattern : unification_constraint) (constraints : list unification_constraint)
|
||
|
||
namespace toy
|
||
constants (A : Type) (f h : A → A) (x y z : A)
|
||
attribute [irreducible]
|
||
noncomputable definition g (x y : A) : A := f z
|
||
|
||
#unify (g x y), (f z)
|
||
|
||
attribute [unify]
|
||
noncomputable definition toy_hint (x y : A) : unification_hint :=
|
||
unification_hint.mk (unification_constraint.mk (g x y) (f z)) []
|
||
|
||
#unify (g x y), (f z)
|
||
print [unify]
|
||
|
||
end toy
|
||
|
||
namespace add
|
||
constants (n : ℕ)
|
||
attribute add [irreducible]
|
||
|
||
#unify (n + 1), succ n
|
||
|
||
attribute [unify]
|
||
definition add_zero_hint (m n : ℕ) [has_add ℕ] [has_one ℕ] [has_zero ℕ] : unification_hint :=
|
||
unification_hint.mk (unification_constraint.mk (m + 1) (succ n)) [unification_constraint.mk m n]
|
||
|
||
#unify (n + 1), (succ n)
|
||
print [unify]
|
||
|
||
end add
|
||
|
||
namespace canonical
|
||
inductive Canonical
|
||
| mk : Π (carrier : Type*) (op : carrier → carrier), Canonical
|
||
|
||
attribute [irreducible]
|
||
definition Canonical.carrier (s : Canonical) : Type* :=
|
||
Canonical.rec_on s (λ c op, c)
|
||
|
||
constants (A : Type) (f : A → A) (x : A)
|
||
noncomputable definition A_canonical : Canonical := Canonical.mk A f
|
||
|
||
#unify (Canonical.carrier A_canonical), A
|
||
|
||
attribute [unify]
|
||
noncomputable definition Canonical_hint (C : Canonical) : unification_hint :=
|
||
unification_hint.mk (unification_constraint.mk (Canonical.carrier C) A) [unification_constraint.mk C A_canonical]
|
||
|
||
-- TODO(dhs): we mark carrier as irreducible and prove A_canonical explicitly to work around the fact that
|
||
-- the default_type_context does not recognize the elaborator metavariables as metavariables,
|
||
-- and so cannot perform the assignment.
|
||
#unify (Canonical.carrier A_canonical), A
|
||
print [unify]
|
||
|
||
end canonical
|