coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: CoqUser CoqUser <coquser AT yahoo.com>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] CoInductive Inheritance using Coercion Problem
- Date: Thu, 23 Apr 2009 11:14:46 -0700 (PDT)
- Domainkey-signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com; h=Message-ID:X-YMail-OSG:Received:X-Mailer:Date:From:Subject:To:MIME-Version:Content-Type; b=uSfy2nroVeQo5k61Ag0uIy2r/JMyEvfdvvibARulFJkvLS7gVWVKwz4lLPRKwzkYNbjqhT3a4+2b9jQuJAhnhgWCZiu84dsOZp7ESfnC7f6xS9L1tTux45WXlh35KKiL71rtwUu8gWnSWB6z5W/Jg7fcYCwyl0TvBuy1/a1aiok=;
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
I want to model inheritance between coinductive types using Coq's Coercion mechanism. Based on the example below, I want the type 'Lexus' to inherit 'paint' and 'isAutomatic' functions from the type 'Car'. How can I do this? Secondly, how can I define a variable of type 'Lexus' and populate it's inherited values for 'paint' and 'isAutomatic'?
Thanks!
(*Simple Example*)
CoInductive Lexus:Set :=
| Build_Lexus (model:string).
CoInductive Car : Type :=
Build_Car (paint:string)(isAutomatic:bool)
| Build_SubTypeLexus (sub:Lexus):>Car. (*Let Lexus inherit from Car.*)
Definition car:Car := Build_Lexus("1234"). (*Lexus is a Car - based on Coercion.*)
Definition lexus:Lexus := Build_Lexus("1234").
Thanks!
(*Simple Example*)
CoInductive Lexus:Set :=
| Build_Lexus (model:string).
CoInductive Car : Type :=
Build_Car (paint:string)(isAutomatic:bool)
| Build_SubTypeLexus (sub:Lexus):>Car. (*Let Lexus inherit from Car.*)
Definition car:Car := Build_Lexus("1234"). (*Lexus is a Car - based on Coercion.*)
Definition lexus:Lexus := Build_Lexus("1234").
- [Coq-Club] CoInductive Inheritance using Coercion Problem, CoqUser CoqUser
- <Possible follow-ups>
- [Coq-Club] CoInductive Inheritance using Coercion Problem, CoqUser CoqUser
Archive powered by MhonArc 2.6.16.