Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- To: M A <tesleft at hotmail.com>
- Subject: Re: [isabelle] which libraries are needed to help to write lemma for operation in functional programming
- From: Lawrence Paulson <lp15 at cam.ac.uk>
- Date: Tue, 28 Oct 2014 12:31:31 +0000
- Cc: isabelle-users <isabelle-users at cl.cam.ac.uk>
- In-reply-to: <BAY167-W92FD07BC2D40E96EABAC38B69F0@phx.gbl>
- References: <BAY167-W3024082D992B681F64185DB69E0@phx.gbl> <, > <, > <BAY167-W27953B618A80B2575F3851B69E0@phx.gbl> <, > <, > <, > <16FFFE45-32C8-44B9-8908-A9471D2F4C7D@uibk.ac.at> <, > <, > <BAY167-W1074477050F04D10DA461BBB69E0@phx.gbl> <, > <, > <alpine.LNX.firstname.lastname@example.org> <, > <BAY167-W1086A25A3C2791880694439B69E0@phx.gbl> <BAY167-W92FD07BC2D40E96EABAC38B69F0@phx.gbl>
I’m afraid that your questions are not very clear. This is partly because of your use of English and partly because you seem to have an unusual application.
I think that you will need to find a colleague who can help you express your questions more clearly.
> On 28 Oct 2014, at 08:34, M A <tesleft at hotmail.com> wrote:
> 1. which libraries are needed to write lemma to find subgoal to observe some functional code?for example, can we import list and complete_lattice or lattice and write associative and distributive lemma and find some subgoals to do functional programming in haskell code for lattice ?
> 2. can three lemmas write into one statement by lemma "(A) ^ (B) V (C)" in order to find algorithms for using 3 lemmas by observe the subgoals?
This archive was generated by a fusion of
Pipermail (Mailman edition) and