lean2/tests/lean/cast4.lean

import cast
set_option pp::colors false

check fun (A A': TypeM)
          (B   : A -> TypeM)
          (B'  : A' -> TypeM)
          (f   : forall x : A, B x)
          (g   : forall x : A', B' x)
          (a   : A)
          (b   : A')
          (H2  : f == g)
          (H3  : a == b),
     hcongr H2 H3
feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-01-05 12:05:08 -08:00			`import cast`
chore(*): cleanup lean builtin symbols, replace :: with _ Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-01-09 08:33:52 -08:00			`set_option pp::colors false`
refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-12-21 18:23:37 -08:00
feat(frontends/lean): use lowercase commands, replace 'endscope' and 'endnamespace' with 'end' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-01-05 12:05:08 -08:00			`check fun (A A': TypeM)`
refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-12-21 18:23:37 -08:00			`(B : A -> TypeM)`
			`(B' : A' -> TypeM)`
feat(kernel): use Pi as forall/implication Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-01-08 00:38:39 -08:00			`(f : forall x : A, B x)`
			`(g : forall x : A', B' x)`
refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2013-12-21 18:23:37 -08:00			`(a : A)`
			`(b : A')`
			`(H2 : f == g)`
			`(H3 : a == b),`
fix(builtin/cast): remove dominj axiom, it is not consistent with the new semantics of Pi/forall Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-01-08 16:19:11 -08:00			`hcongr H2 H3`