MCPcopy Create free account
hub / github.com/agenticsorg/lean-agentic / test_simple_def

Function test_simple_def

leanr-syntax/src/parser.rs:742–754  ·  view source on GitHub ↗
()

Source from the content-addressed store, hash-verified

740
741 #[test]
742 fn test_simple_def() {
743 let input = "def id (x : Nat) : Nat := x";
744 let decls = parse(input).unwrap();
745 assert_eq!(decls.len(), 1);
746
747 match &decls[0] {
748 Decl::Def(def) => {
749 assert_eq!(def.name.name, "id");
750 assert_eq!(def.params.len(), 1);
751 }
752 _ => panic!("Expected def"),
753 }
754 }
755
756 #[test]
757 fn test_lambda() {

Callers

nothing calls this directly

Calls 1

parseFunction · 0.85

Tested by

no test coverage detected