2014-12-01 05:16:01 +00:00
|
|
|
prelude definition Prop : Type.{1} := Type.{0}
|
2014-06-14 00:30:35 +00:00
|
|
|
section
|
2014-10-09 14:13:06 +00:00
|
|
|
variable {A : Type} -- Mark A as implicit parameter
|
|
|
|
|
variable R : A → A → Prop
|
2014-06-14 00:30:35 +00:00
|
|
|
definition id (a : A) : A := a
|
2014-07-22 16:43:18 +00:00
|
|
|
definition refl : Prop := forall (a : A), R a a
|
|
|
|
|
definition symm : Prop := forall (a b : A), R a b -> R b a
|
2014-06-14 00:30:35 +00:00
|
|
|
end
|
|
|
|
|
check id.{2}
|
|
|
|
|
check refl.{1}
|
|
|
|
|
check symm.{1}
|
