()
| 762 | |
| 763 | #[test] |
| 764 | fn test_inductive() { |
| 765 | let input = r#" |
| 766 | inductive Nat where |
| 767 | | zero : Nat |
| 768 | | succ (n : Nat) : Nat |
| 769 | "#; |
| 770 | let decls = parse(input).unwrap(); |
| 771 | assert_eq!(decls.len(), 1); |
| 772 | |
| 773 | match &decls[0] { |
| 774 | Decl::Inductive(ind) => { |
| 775 | assert_eq!(ind.name.name, "Nat"); |
| 776 | assert_eq!(ind.constructors.len(), 2); |
| 777 | } |
| 778 | _ => panic!("Expected inductive"), |
| 779 | } |
| 780 | } |
| 781 | } |