Default values in structure

Stream: new members

[Markus Schmaus]

Mathlib defines a PythagoreanTriple property, I now want to define a PythogoreanTriples type based on it (analog to Nat.Prime and Nat.Primes).

import Mathlib

instance : Decidable (PythagoreanTriple x y z) := inferInstanceAs <| Decidable (_ = _)

structure PythagoreanTriples where
  x : ℤ
  y : ℤ
  z : ℤ
  property : PythagoreanTriple x y z := by decide
deriving DecidableEq, Repr

def a : PythagoreanTriples := {x := 3, y := 4, z := 5}
def b := PythagoreanTriples.mk 3 4 5
-- def c : PythagoreanTriples := ⟨3, 4, 5⟩

def a and def b work, but def c raises and error. How can I make def c work?

[Notification Bot]

Markus Schmaus has marked this topic as unresolved.

[Eric Wieser]

A simpler example is:

structure Two where
  x : Nat
  property : x = 2 := by decide

def c : Two := ⟨2⟩ --fails

This might be a question for #lean4 in that minimized state