(lean_env: &LeanEnv)
| 2955 | KConst::Axio { |
| 2956 | name: self_name.clone(), |
| 2957 | level_params: pn.clone(), |
| 2958 | is_unsafe: v.is_unsafe, |
| 2959 | lvls: pn.len() as u64, |
| 2960 | ty: expr_to_k(&v.cnst.typ, pn), |
| 2961 | } |
| 2962 | }, |
| 2963 | LeanCI::DefnInfo(v) => { |
| 2964 | let pn = &v.cnst.level_params; |
| 2965 | let all = Some(&v.all); |
| 2966 | KConst::Defn { |
| 2967 | name: self_name.clone(), |
| 2968 | level_params: pn.clone(), |
| 2969 | kind: DefKind::Definition, |
| 2970 | safety: v.safety, |
| 2971 | hints: v.hints, |
| 2972 | lvls: pn.len() as u64, |
| 2973 | ty: expr_to_k(&v.cnst.typ, pn), |
| 2974 | val: expr_to_k(&v.value, pn), |
| 2975 | lean_all: lean_all_ids(&v.all, n2a), |
| 2976 | block: lean_block_id(self_name, all, n2a), |
| 2977 | } |
| 2978 | }, |
| 2979 | LeanCI::ThmInfo(v) => { |
| 2980 | let pn = &v.cnst.level_params; |
| 2981 | let all = Some(&v.all); |
| 2982 | KConst::Defn { |
| 2983 | name: self_name.clone(), |
| 2984 | level_params: pn.clone(), |
| 2985 | kind: DefKind::Theorem, |
| 2986 | safety: DefinitionSafety::Safe, |
| 2987 | hints: ReducibilityHints::Opaque, |
| 2988 | lvls: pn.len() as u64, |
| 2989 | ty: expr_to_k(&v.cnst.typ, pn), |
| 2990 | val: expr_to_k(&v.value, pn), |
| 2991 | lean_all: lean_all_ids(&v.all, n2a), |
| 2992 | block: lean_block_id(self_name, all, n2a), |
| 2993 | } |
| 2994 | }, |
| 2995 | LeanCI::OpaqueInfo(v) => { |
| 2996 | let pn = &v.cnst.level_params; |
| 2997 | let all = Some(&v.all); |
| 2998 | KConst::Defn { |
| 2999 | name: self_name.clone(), |
| 3000 | level_params: pn.clone(), |
| 3001 | kind: DefKind::Opaque, |
| 3002 | safety: if v.is_unsafe { |
| 3003 | DefinitionSafety::Unsafe |
| 3004 | } else { |
| 3005 | DefinitionSafety::Safe |
| 3006 | }, |
| 3007 | hints: ReducibilityHints::Opaque, |
| 3008 | lvls: pn.len() as u64, |
| 3009 | ty: expr_to_k(&v.cnst.typ, pn), |
| 3010 | val: expr_to_k(&v.value, pn), |
| 3011 | lean_all: lean_all_ids(&v.all, n2a), |
| 3012 | block: lean_block_id(self_name, all, n2a), |
| 3013 | } |
| 3014 | }, |
no test coverage detected