21 lines
1.3 KiB
Text
21 lines
1.3 KiB
Text
"(Term.id `Nat.one.0 (null))"
|
|
"<missing>"
|
|
"<missing>"
|
|
"<missing>"
|
|
"(Term.add <missing> \"+\" (Term.num (numLit \"1\")))"
|
|
"(Term.add <missing> \"+\" (Term.num (numLit \"1\")))"
|
|
"(Term.add (Term.num (numLit \"1\")) \"+\" (Term.num (numLit \"1\")))"
|
|
"(Term.fun \"fun\" (null (Term.id `a.0 (null))) \"=>\" (Term.id `a.0 (null)))"
|
|
"(Term.id `Nat.one.0 (null))"
|
|
"(Term.app (Term.app (Term.id `f.0 (null)) (Term.id `Nat.one.0 (null))) (Term.id `Nat.one.0 (null)))"
|
|
"(Term.dollar\n (Term.id `f.0 (null))\n \"$\"\n (Term.app (Term.app (Term.id `f.0 (null)) (Term.id `Nat.one.0 (null))) (Term.num (numLit \"1\"))))"
|
|
"(Term.app (Term.id `f.0 (null)) (Term.id `Nat.one.0 (null)))"
|
|
"(Term.add (Term.num (numLit \"2\")) \"+\" (Term.num (numLit \"1\")))"
|
|
"0"
|
|
"1"
|
|
"(Term.fun\n \"fun\"\n (null\n (Term.id `a.0 (null))\n (Term.paren \"(\" (null (Term.id `b.0 (null)) (null (Term.typeAscription \":\" (Term.id `Nat.0 (null))))) \")\"))\n \"=>\"\n (Term.num (numLit \"1\")))"
|
|
"#[(Term.paren \"(\" (null (Term.id `a.0 (null)) (null (Term.typeAscription \":\" (Term.id `Nat.0 (null))))) \")\"), (Term.id `b.0 (null))]"
|
|
"`a.0"
|
|
"(Term.forall \"∀\" (null (Term.simpleBinder (null (Term.hole \"_\")))) \",\" (Term.id `c.0 (null)))"
|
|
"`a.0"
|
|
"(Term.id `a.0 (null (Term.explicitUniv \".{\" (null (Level.num (numLit \"0\"))) \"}\")))"
|