Who Cites sfa doc sexpr cases? | |
sfa_doc_sexpr_cases | Def == InjCase(s; s1s2. s1s2/s1,s2. f(s1;s2); x. g(x)) |
Thm* f:(s1,s2:Sexpr(A)C(Cons(s1;s2))), g:(x:AC(Inj(x))). Thm* (Case of s : Inj(x) g(x) ; Cons(s1;s2) f(s1,s2)) C(s) |
Syntax: | has structure: |
About: