pub struct IdrisData {
pub name: String,
pub params: Vec<(String, IdrisType)>,
pub kind: IdrisType,
pub constructors: Vec<IdrisConstructor>,
pub visibility: Visibility,
pub doc: Option<String>,
}Expand description
A data declaration in Idris 2.
Fields§
§name: StringType name.
params: Vec<(String, IdrisType)>Type parameters: (a : Type), (n : Nat).
kind: IdrisTypeThe kind of this type (usually Type).
constructors: Vec<IdrisConstructor>Constructors.
visibility: VisibilityVisibility.
doc: Option<String>Optional doc comment.
Implementations§
Trait Implementations§
impl StructuralPartialEq for IdrisData
Auto Trait Implementations§
impl Freeze for IdrisData
impl RefUnwindSafe for IdrisData
impl Send for IdrisData
impl Sync for IdrisData
impl Unpin for IdrisData
impl UnsafeUnpin for IdrisData
impl UnwindSafe for IdrisData
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more