-- This file:
--   http://anggtwu.net/LEAN/structures1.lean.html
--   http://anggtwu.net/LEAN/structures1.lean
--          (find-angg "LEAN/structures1.lean")
-- Author: Eduardo Ochs <eduardoochs@gmail.com>
--
-- (defun e () (interactive) (find-angg "LEAN/structures1.lean"))
-- (find-fplean4page 18 "Structures")
-- (find-fplean4text 18 "Structures")
-- (find-fplean4page 21 "Updating Structures")
-- (find-fplean4text 21 "Updating Structures")
-- (find-fplean4page 23 "Point.point instead of Point.mk")
-- (find-fplean4text 23 "Point.point instead of Point.mk")
-- (find-fplean4page 23 "TARGET.f ARG1 ARG2 ...")
-- (find-fplean4text 23 "TARGET.f ARG1 ARG2 ...")
-- (find-fplean4page 130 "Deriving Standard Classes")
-- (find-fplean4text 130 "Deriving Standard Classes")
-- (find-fplean4page 131 "instance : Append")
-- (find-fplean4text 131 "instance : Append")


structure Point where
  x : Float
  y : Float
  deriving Repr

def p : Point := { x := 1, y := 2 }
#eval p
#print Point
#print Point.x
#print Point.mk

#eval p.x

#eval {p with x := 3}

structure S1 where
  a : Nat
  b : Nat
structure S2 where
  mymk ::
  a : Nat
  b : Nat
structure S3 where         ( a : Nat ) ( b : Nat )
structure S4 where mymk :: ( a : Nat ) ( b : Nat )
#print S1
#print S2
#print S3
#print S4



-- structure S2 where { a : Nat } { b : Nat }


-- Local Variables:
-- coding:  utf-8-unix
-- End: