is mentioned by
[sfa_doc_sexpr_fp] | |
[sfa_doc_fun_ext] | |
[sfa_doc_reinject] | |
[sfa_doc_listify_select_id] | |
[sfa_doc_pairing_projs] | |
[sfa_doc_type_poly_swap] | |
[sfa_doc_type_poly_ap_doppelganger] | |
[sfa_doc_top_is_top] | |
[sfa_doc_whatever_in_void_dom_fun] | |
[sfa_doc_void_dom_fun_degenerate] | |
[sfa_doc_void_is_bottom] | |
[sfa_doc_void_cross_is_void] | |
[sfa_doc_polymorph_example1] | |
[sfa_doc_int_sub_int_mod] | |
[sfa_doc_type_poly_constant] | |
[sfa_doc_type_poly_identity] | |
Thm* ||f(a)|| = ||f(b)|| | [sfa_doc_type_poly_len_const] |
[sfa_doc_type_poly_mem_const] | |
[sfa_doc_inlist_singleton_const] | |
[sfa_doc_inlist_wf] | |
[sfa_doc_nat_sqrt] | |
[sfa_doc_sequence_rel_wf] | |
[sfa_doc_greater_list_bound_wf] | |
[sfa_doc_eq_mem_unique] | |
[sfa_doc_isect_subtype] | |
[sfa_doc_bool_vs_decidable_fun] | |
[sfa_doc_bool_vs_decidable] | |
Thm* (x:. f zero beyond x) & (x:. g zero beyond x) Thm* Thm* (x:. (i.if i even f(i) else g(i) fi) zero beyond x) | [sfa_doc_alternate_zero_beyond] |
[sfa_doc_max_int_wf] | |
[sfa_doc_even_wf] | |
[sfa_doc_props_as_types_example1_wf] | |
[sfa_doc_or_dec] | |
Thm* (n:. f(n) = 0) Thm* Thm* (n:. if f(n)=0 False else C:Prop{1}. C fi) Prop{1} | [sfa_doc_predicativity_sample8] |
Thm* P:((A List)Prop). Thm* (P(nil) Q) & (a:A, x:A List. P(a.x) R(a,x,P(x))) | [sfa_doc_listind_via_so] |
[sfa_doc_equal_via_so] | |
[sfa_doc_some_via_so] | |
[sfa_doc_false_via_so] | |
[sfa_doc_iff_via_so] | |
[sfa_doc_not_via_so] | |
[sfa_doc_or_via_so] | |
[sfa_doc_and_via_so] | |
[sfa_doc_guarded_typing] | |
[sfa_doc_imp_typing] | |
Thm* Reverse(Cons(Inj(a);Cons(Inj(b);Inj(c)))) Thm* = Thm* Cons(Cons(Inj(c);Inj(b));Inj(a)) | [sfa_doc_sexpr_reverse_example] |
[sfa_doc_sexpr_reverse_wf] | |
[sfa_doc_sexpr_atom_wf] | |
[sfa_doc_sexprcdrsize] | |
[sfa_doc_sexprcarsize] | |
[sfa_doc_sexpr_size_wf] | |
[sfa_doc_sexpr_cdr_wf] | |
[sfa_doc_sexpr_car_wf] | |
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) | [sfa_doc_sexpr_cases_wf] |
[sfa_doc_sexpr_case_thm] | |
[sfa_doc_sexpr_inj_wf] | |
[sfa_doc_sexpr_cons_wf] | |
[sfa_doc_sexpr_wf] | |
[sfa_doc_ntuple_contains_wf] | |
[sfa_doc_ntuple_is_prod] | |
[sfa_doc_ntuple_wf] | |
[sfa_doc_factorial2_wf] | |
[sfa_doc_factorial_wf] | |
[sfa_doc_memtype_is_singleton] | |
[sfa_doc_sample_intmod_wf] | |
[sfa_doc_and_typing] | |
[sfa_doc_cand_example] | |
[sfa_doc_indep_fun_typing] | |
Thm* x:{u:A| P(u) }B(x) =ext x:AB(x)(given P(x)) | [sfa_doc_exteq_gfun2] |
Thm* x:{u:A| B(u) }C(x) =ext x:AC(x)(given B(x)) | [sfa_doc_exteq_gfun] |
[sfa_doc_exteq_gprop] | |
[kleene_minimize_is_lb] | |
[kleene_minimize_is_fp] | |
[kleene_tail] | |
[sfa_doc_greater_list_bound] | |
[sfa_doc_props_as_types_example1] | |
[sfa_doc_indscheme] | |
[sfa_doc_exteq] |
In prior sections: core well fnd int 1 bool 1 rel 1 union fun 1 int 2 list 1 sqequal 1
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html