Perhaps try `!x. (inv x) prod x = unit`
My guess is that your term is being parsed incorrectly, leading something
that's not x to be interpreted as a variable and assigned a variable type,
which then makes the types of the two sides of the equation unequal.
On Tue, May 15, 2012 at 3:53 AM, Bill Richter <[email protected]
> wrote:
> Trying to improve my group theory code, I tried to use new_axiom, and
> I could not get this to work. Help!
>
> (* this works fine *)
>
> new_type("element",0);;
> new_constant("prod",`:element->element->element`);;
> new_constant("inv",`:element->element`);;
> new_constant("unit",`:element`);;
> parse_as_infix("prod",(20, "right"));;
>
> let A1 = new_axiom
> `!x y z. (x prod y) prod z = x prod (y prod z)`;;
>
> let left_unit = new_axiom
> `!x . unit prod x = x`;;
>
> (* This does not: *)
>
> let left_inv = new_axiom
> `!x . inv(x) prod x = unit`;;
>
> (* Exception: Failure "typechecking error (initial type assignment)". *)
>
> --
> Best,
> Bill
>
>
> ------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
