lean2/tests/lean/t7.lean.expected.out

id : ?M_1 → ?M_1
trans : (?M_1 → ?M_1 → Prop) → Prop
symm : (?M_1 → ?M_1 → Prop) → Prop
equivalence : (?M_1 → ?M_1 → Prop) → Prop
λ {A : Type} (R : A → A → Prop),
  and (and (refl R) (symm R)) (trans R)
feat(frontends/lean): add basic pretty printer Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-09 08:12:36 +00:00			`id : ?M_1 → ?M_1`
refactor(*): rename Bool to Prop Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-22 16:43:18 +00:00			`trans : (?M_1 → ?M_1 → Prop) → Prop`
			`symm : (?M_1 → ?M_1 → Prop) → Prop`
			`equivalence : (?M_1 → ?M_1 → Prop) → Prop`
fix(frontends/lean/pp): bug when pretty printing binder information, fixes #73 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-08-21 16:28:07 +00:00			`λ {A : Type} (R : A → A → Prop),`
feat(frontends/lean): add let-expr pretty printer, reduce default indentation to 2 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-10 01:47:10 +00:00			`and (and (refl R) (symm R)) (trans R)`